Theorem mpan2d 706

Description: A deduction based on modus ponens.

Hypotheses

Ref	Expression
mpan2d.1	⊢ (φ → χ)
mpan2d.2	⊢ (φ → ((ψ ⋀ χ) → θ))

Assertion

Ref	Expression
mpan2d	⊢ (φ → (ψ → θ))

Proof of Theorem mpan2d

Step	Hyp	Ref	Expression
1		mpan2d.1	. 2 ⊢ (φ → χ)
2		mpan2d.2	. . 3 ⊢ (φ → ((ψ ⋀ χ) → θ))
3	2	exp3a 376	. 2 ⊢ (φ → (ψ → (χ → θ)))
4	1, 3	mpid 47	1 ⊢ (φ → (ψ → θ))

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  alephle 4897  xrret 5582  xrre2t 5583  letrp1t 5820  ledivp1t 5911  xrltmint 5920  lemint 5927  xrinfmsslem 6083  peano2uz2 6210  uzind 6214  flget 6242  qbtwnxr 6290  monoord 6305  elioc2t 6339  elico2t 6340  elicc2t 6341  fzss2t 6454  fsequb 6473  ser1add2 6521  ser1add 6522  leabst 6878  seq1bnd 6924  cvg2 6936  caubnd 6940  facwordit 6958  facavgt 6969  clm4le 7095  2climnn 7116  2climnn0 7117  climmullem5 7138  ser1cmp2lem 7190  ivthlem6 7300  ivthlem7 7301  metcnpi3 7901  metcnpi4 7902  metcni2 7904  bcthlem2 8009  nmoub3i 8444  minveceu 8591  shsel1t 9292  sumspansnt 9601  nmopub2tALT 9840  nmfnleub2t 9857

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain