Theorem mpand 703

Description: A deduction based on modus ponens.

Hypotheses

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

Assertion

Ref	Expression
mpand	⊢ (φ → (χ → θ))

Proof of Theorem mpand

Step	Hyp	Ref	Expression
1		mpand.1	. 2 ⊢ (φ → ψ)
2		mpand.2	. . 3 ⊢ (φ → ((ψ ⋀ χ) → θ))
3	2	exp3a 376	. 2 ⊢ (φ → (ψ → (χ → θ)))
4	1, 3	mpd 26	1 ⊢ (φ → (χ → θ))

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  mp2and 705  orduniorsuc 3093  xrre2t 5582  p1let 5819  xrmaxltt 5915  maxlet 5920  maxltt 5924  nnge1t 5945  xrsupsslem 6078  xrub 6082  supxrunb1 6091  gtndivt 6195  flwordit 6239  ceilet 6252  qbtwnxr 6280  ser1add2 6339  ser1add 6340  elioc2t 6391  elico2t 6392  elicc2t 6393  uzss 6432  fzss1t 6504  seq1ublem 6911  cvganz 6924  caubnd 6926  caure 6927  cauim 6928  ser1absdiflem 6929  facavgt 6955  bccl2t 6971  fsumsplit 7020  clm3 7079  2climnn 7102  2climnn0 7103  climaddlem3 7116  climmullem8 7127  climsqueeze 7140  climsqueeze2 7141  climabslem 7148  climcau 7156  caucvglem6 7162  caucvg 7163  serzf0 7169  ser1f0 7170  cvgcmp3c 7186  reccnv 7218  cvgratlem4 7253  ivthlem7 7287  efaddlem23 7360  infpn2 7510  lmnn 7932  iscau3 7935  iscau4 7937  lmuni 7948  lmcau 7993  bcthlem21 8016  bcthlem25 8020  grpidinvlem3 8047  grpideu 8050  nmcnilem 8333  blocni 8461  minveclem25 8565  minveclem27 8567  htthlem10 8625  hcau2 9050  occllem6 9173  osumlem4 9576  sumspansnt 9589  pjnmop 10070  hmopidmch 10074  atoml 10304  sumdmdlem2 10341  cdj3lem2b 10359

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