Theorem mpand 429

Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

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	ancomsd 269	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))
4	1, 3	mpan2d 428	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpani  430  mp2and  433  rspcimedv  2925  ovig  6177  prcdnql  7804  prcunqu  7805  p1le  9128  nnge1  9265  zltp1le  9637  gtndiv  9679  uzss  9881  addlelt  10107  xrre2  10160  xrre3  10161  zltaddlt1le  10347  nn0p1elfzo  10528  zsupcllemstep  10596  modfzo0difsn  10764  seqf1oglem1  10888  leexp2r  10962  expnlbnd2  11035  facavg  11116  wrdred1hash  11276  ccat2s1fvwd  11343  caubnd2  11810  maxleast  11906  mulcn2  12005  cn1lem  12007  climsqz  12028  climsqz2  12029  climcvg1nlem  12042  fsumabs  12159  cvgratnnlemnexp  12218  cvgratnnlemmn  12219  bitsfzolem  12648  bitsfzo  12649  gcdzeq  12726  algcvgblem  12754  algcvga  12756  lcmdvdsb  12789  coprm  12849  pclemub  12993  bldisj  15315  xblm  15331  metss2lem  15411  bdxmet  15415  limccoap  15592  lgsne0  15960  gausslemma2dlem1a  15980  eupth2lemsfi  16522