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  4680  tfr0dm  6479  tfr1onlemaccex  6505  tfrcllemaccex  6518  ertrd  6709  th3qlem1  6797  en2prd  6983  findcard2  7064  findcard2s  7065  diffifi  7069  fimax2gtrilemstep  7076  fidcenumlemrk  7137  fidcenumlemr  7138  isbth  7150  nninfninc  7306  cc2lem  7468  ltbtwnnqq  7618  prarloclemarch2  7622  addlocprlemeqgt  7735  addnqprlemrl  7760  addnqprlemru  7761  mulnqprlemrl  7776  mulnqprlemru  7777  ltexprlemrl  7813  ltexprlemru  7815  addcanprleml  7817  addcanprlemu  7818  recexprlemloc  7834  recexprlem1ssu  7837  cauappcvgprlemladdfl  7858  caucvgprlemloc  7878  caucvgprprlemloccalc  7887  letrd  8286  lelttrd  8287  lttrd  8288  ltletrd  8586  le2addd  8726  le2subd  8727  ltleaddd  8728  leltaddd  8729  lt2subd  8731  ltmul12a  9023  lediv12a  9057  lemul12ad  9105  lemul12bd  9106  lt2halvesd  9375  uzind  9574  uztrn  9756  xrlttrd  10022  xrlelttrd  10023  xrltletrd  10024  xrletrd  10025  ixxss1  10117  ixxss2  10118  ixxss12  10119  zsupcllemex  10467  zssinfcl  10469  fldiv4p1lem1div2  10542  seqf1og  10760  faclbnd3  10982  abs3lemd  11733  xrbdtri  11808  modfsummod  11990  mertenslemi1  12067  sin01gt0  12294  cos01gt0  12295  sin02gt0  12296  dvds2subd  12359  dvds2addd  12361  dvdstrd  12362  bezoutlemstep  12539  mulgcd  12558  gcddvdslcm  12616  lcmgcdeq  12626  mulgcddvds  12637  rpmulgcd2  12638  rpdvds  12642  divgcdcoprmex  12645  rpexp  12696  phimullem  12768  eulerthlem1  12770  eulerthlemrprm  12772  eulerthlemth  12775  prmdiveq  12779  pythagtriplem4  12812  pcqmul  12847  pcgcd1  12872  pcadd  12884  pockthlem  12900  4sqlem16  12950  exmidunben  13018  mulgass  13717  lmtopcnp  14945  blin2  15127  xmetxp  15202  tgqioo  15250  cncfmptid  15292  negcncf  15300  limcimolemlt  15359  plyadd  15446  plymul  15447  sinq12gt0  15525  logdivlti  15576  mpodvdsmulf1o  15685  perfectlem1  15694  2sqlem5  15819  2sqlem8  15823