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  6597  tfr1onlemaccex  6623  tfrcllemaccex  6636  ertrd  6827  th3qlem1  6915  en2prd  7111  findcard2  7198  findcard2s  7199  diffifi  7203  fimax2gtrilemstep  7210  fidcenumlemrk  7277  fidcenumlemr  7278  isbth  7290  nninfninc  7470  cc2lem  7639  ltbtwnnqq  7789  prarloclemarch2  7793  addlocprlemeqgt  7906  addnqprlemrl  7931  addnqprlemru  7932  mulnqprlemrl  7947  mulnqprlemru  7948  ltexprlemrl  7984  ltexprlemru  7986  addcanprleml  7988  addcanprlemu  7989  recexprlemloc  8005  recexprlem1ssu  8008  cauappcvgprlemladdfl  8029  caucvgprlemloc  8049  caucvgprprlemloccalc  8058  letrd  8458  lelttrd  8459  lttrd  8460  ltletrd  8759  le2addd  8900  le2subd  8901  ltleaddd  8902  leltaddd  8903  lt2subd  8905  ltmul12a  9199  lediv12a  9233  lemul12ad  9281  lemul12bd  9282  lt2halvesd  9565  uzind  9769  uztrn  9956  xrlttrd  10229  xrlelttrd  10230  xrltletrd  10231  xrletrd  10232  ixxss1  10324  ixxss2  10325  ixxss12  10326  zsupcllemex  10681  zssinfcl  10683  fldiv4p1lem1div2  10762  seqf1og  10980  faclbnd3  11204  abs3lemd  11991  xrbdtri  12068  modfsummod  12251  mertenslemi1  12328  sin01gt0  12555  cos01gt0  12556  sin02gt0  12557  dvds2subd  12620  dvds2addd  12622  dvdstrd  12623  bezoutlemstep  12800  mulgcd  12819  gcddvdslcm  12877  lcmgcdeq  12887  mulgcddvds  12898  rpmulgcd2  12899  rpdvds  12903  divgcdcoprmex  12906  rpexp  12958  phimullem  13033  eulerthlem1  13035  eulerthlemrprm  13037  eulerthlemth  13040  prmdiveq  13044  pythagtriplem4  13077  pcqmul  13112  pcgcd1  13137  pcadd  13149  pockthlem  13165  4sqlem16  13215  exmidunben  13376  mulgass  14022  gsumbagdiaglem  15180  lmtopcnp  15488  blin2  15670  xmetxp  15745  tgqioo  15793  cncfmptid  15835  negcncf  15843  limcimolemlt  15902  plyadd  15989  plymul  15990  sinq12gt0  16069  logdivlti  16123  ppiprm  16271  mpodvdsmulf1o  16296  perfectlem1  16311  2sqlem5  16455  2sqlem8  16459