Theorem mp2and 437

Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)

Hypotheses

Ref	Expression
mp2and.1	⊢ (𝜑 → 𝜓)
mp2and.2	⊢ (𝜑 → 𝜒)
mp2and.3	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
mp2and	⊢ (𝜑 → 𝜃)

Proof of Theorem mp2and

Step	Hyp	Ref	Expression
1		mp2and.2	. 2 ⊢ (𝜑 → 𝜒)
2		mp2and.1	. . 3 ⊢ (𝜑 → 𝜓)
3		mp2and.3	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
4	2, 3	mpand 433	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5	1, 4	mpd 13	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  tfisi  4736  tfr0dm  6598  tfr1onlemaccex  6624  tfrcllemaccex  6637  ertrd  6828  th3qlem1  6916  en2prd  7112  findcard2  7199  findcard2s  7200  diffifi  7204  fimax2gtrilemstep  7211  fidcenumlemrk  7278  fidcenumlemr  7279  isbth  7291  nninfninc  7469  cc2lem  7638  ltbtwnnqq  7788  prarloclemarch2  7792  addlocprlemeqgt  7905  addnqprlemrl  7930  addnqprlemru  7931  mulnqprlemrl  7946  mulnqprlemru  7947  ltexprlemrl  7983  ltexprlemru  7985  addcanprleml  7987  addcanprlemu  7988  recexprlemloc  8004  recexprlem1ssu  8007  cauappcvgprlemladdfl  8028  caucvgprlemloc  8048  caucvgprprlemloccalc  8057  letrd  8457  lelttrd  8458  lttrd  8459  ltletrd  8758  le2addd  8899  le2subd  8900  ltleaddd  8901  leltaddd  8902  lt2subd  8904  ltmul12a  9198  lediv12a  9232  lemul12ad  9280  lemul12bd  9281  lt2halvesd  9564  uzind  9767  uztrn  9954  xrlttrd  10227  xrlelttrd  10228  xrltletrd  10229  xrletrd  10230  ixxss1  10322  ixxss2  10323  ixxss12  10324  zsupcllemex  10679  zssinfcl  10681  fldiv4p1lem1div2  10760  seqf1og  10978  faclbnd3  11202  abs3lemd  11989  xrbdtri  12066  modfsummod  12249  mertenslemi1  12326  sin01gt0  12553  cos01gt0  12554  sin02gt0  12555  dvds2subd  12618  dvds2addd  12620  dvdstrd  12621  bezoutlemstep  12798  mulgcd  12817  gcddvdslcm  12875  lcmgcdeq  12885  mulgcddvds  12896  rpmulgcd2  12897  rpdvds  12901  divgcdcoprmex  12904  rpexp  12956  phimullem  13031  eulerthlem1  13033  eulerthlemrprm  13035  eulerthlemth  13038  prmdiveq  13042  pythagtriplem4  13075  pcqmul  13110  pcgcd1  13135  pcadd  13147  pockthlem  13163  4sqlem16  13213  exmidunben  13374  mulgass  14020  gsumbagdiaglem  15184  lmtopcnp  15493  blin2  15675  xmetxp  15750  tgqioo  15798  cncfmptid  15840  negcncf  15848  limcimolemlt  15907  plyadd  15994  plymul  15995  sinq12gt0  16074  logdivlti  16128  ppiprm  16276  mpodvdsmulf1o  16301  perfectlem1  16316  2sqlem5  16460  2sqlem8  16464