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  4601  tfr0dm  6341  tfr1onlemaccex  6367  tfrcllemaccex  6380  ertrd  6569  th3qlem1  6655  findcard2  6907  findcard2s  6908  diffifi  6912  fimax2gtrilemstep  6918  fidcenumlemrk  6971  fidcenumlemr  6972  isbth  6984  cc2lem  7283  ltbtwnnqq  7432  prarloclemarch2  7436  addlocprlemeqgt  7549  addnqprlemrl  7574  addnqprlemru  7575  mulnqprlemrl  7590  mulnqprlemru  7591  ltexprlemrl  7627  ltexprlemru  7629  addcanprleml  7631  addcanprlemu  7632  recexprlemloc  7648  recexprlem1ssu  7651  cauappcvgprlemladdfl  7672  caucvgprlemloc  7692  caucvgprprlemloccalc  7701  letrd  8099  lelttrd  8100  lttrd  8101  ltletrd  8398  le2addd  8538  le2subd  8539  ltleaddd  8540  leltaddd  8541  lt2subd  8543  ltmul12a  8835  lediv12a  8869  lemul12ad  8917  lemul12bd  8918  lt2halvesd  9184  uzind  9382  uztrn  9562  xrlttrd  9827  xrlelttrd  9828  xrltletrd  9829  xrletrd  9830  ixxss1  9922  ixxss2  9923  ixxss12  9924  fldiv4p1lem1div2  10323  faclbnd3  10741  abs3lemd  11228  xrbdtri  11302  modfsummod  11484  mertenslemi1  11561  sin01gt0  11787  cos01gt0  11788  sin02gt0  11789  dvds2subd  11852  dvds2addd  11854  dvdstrd  11855  zsupcllemex  11965  zssinfcl  11967  bezoutlemstep  12016  mulgcd  12035  gcddvdslcm  12091  lcmgcdeq  12101  mulgcddvds  12112  rpmulgcd2  12113  rpdvds  12117  divgcdcoprmex  12120  rpexp  12171  phimullem  12243  eulerthlem1  12245  eulerthlemrprm  12247  eulerthlemth  12250  prmdiveq  12254  pythagtriplem4  12286  pcqmul  12321  pcgcd1  12345  pcadd  12357  pockthlem  12372  exmidunben  12445  mulgass  13065  lmtopcnp  14147  blin2  14329  xmetxp  14404  tgqioo  14444  cncfmptid  14480  negcncf  14485  limcimolemlt  14530  sinq12gt0  14648  logdivlti  14699  2sqlem5  14863  2sqlem8  14867