Theorem mp2and 433

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 429	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5	1, 4	mpd 13	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:  tfisi  4708  tfr0dm  6552  tfr1onlemaccex  6578  tfrcllemaccex  6591  ertrd  6782  th3qlem1  6870  en2prd  7058  findcard2  7145  findcard2s  7146  diffifi  7150  fimax2gtrilemstep  7157  fidcenumlemrk  7223  fidcenumlemr  7224  isbth  7236  nninfninc  7413  cc2lem  7576  ltbtwnnqq  7726  prarloclemarch2  7730  addlocprlemeqgt  7843  addnqprlemrl  7868  addnqprlemru  7869  mulnqprlemrl  7884  mulnqprlemru  7885  ltexprlemrl  7921  ltexprlemru  7923  addcanprleml  7925  addcanprlemu  7926  recexprlemloc  7942  recexprlem1ssu  7945  cauappcvgprlemladdfl  7966  caucvgprlemloc  7986  caucvgprprlemloccalc  7995  letrd  8393  lelttrd  8394  lttrd  8395  ltletrd  8693  le2addd  8833  le2subd  8834  ltleaddd  8835  leltaddd  8836  lt2subd  8838  ltmul12a  9130  lediv12a  9164  lemul12ad  9212  lemul12bd  9213  lt2halvesd  9482  uzind  9685  uztrn  9867  xrlttrd  10138  xrlelttrd  10139  xrltletrd  10140  xrletrd  10141  ixxss1  10233  ixxss2  10234  ixxss12  10235  zsupcllemex  10586  zssinfcl  10588  fldiv4p1lem1div2  10661  seqf1og  10879  faclbnd3  11101  abs3lemd  11879  xrbdtri  11954  modfsummod  12137  mertenslemi1  12214  sin01gt0  12441  cos01gt0  12442  sin02gt0  12443  dvds2subd  12506  dvds2addd  12508  dvdstrd  12509  bezoutlemstep  12686  mulgcd  12705  gcddvdslcm  12763  lcmgcdeq  12773  mulgcddvds  12784  rpmulgcd2  12785  rpdvds  12789  divgcdcoprmex  12792  rpexp  12843  phimullem  12915  eulerthlem1  12917  eulerthlemrprm  12919  eulerthlemth  12922  prmdiveq  12926  pythagtriplem4  12959  pcqmul  12994  pcgcd1  13019  pcadd  13031  pockthlem  13047  4sqlem16  13097  exmidunben  13166  mulgass  13865  lmtopcnp  15102  blin2  15284  xmetxp  15359  tgqioo  15407  cncfmptid  15449  negcncf  15457  limcimolemlt  15516  plyadd  15603  plymul  15604  sinq12gt0  15682  logdivlti  15733  mpodvdsmulf1o  15845  perfectlem1  15854  2sqlem5  15979  2sqlem8  15983