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  4639  tfr0dm  6415  tfr1onlemaccex  6441  tfrcllemaccex  6454  ertrd  6643  th3qlem1  6731  en2prd  6916  findcard2  6993  findcard2s  6994  diffifi  6998  fimax2gtrilemstep  7004  fidcenumlemrk  7063  fidcenumlemr  7064  isbth  7076  nninfninc  7232  cc2lem  7385  ltbtwnnqq  7535  prarloclemarch2  7539  addlocprlemeqgt  7652  addnqprlemrl  7677  addnqprlemru  7678  mulnqprlemrl  7693  mulnqprlemru  7694  ltexprlemrl  7730  ltexprlemru  7732  addcanprleml  7734  addcanprlemu  7735  recexprlemloc  7751  recexprlem1ssu  7754  cauappcvgprlemladdfl  7775  caucvgprlemloc  7795  caucvgprprlemloccalc  7804  letrd  8203  lelttrd  8204  lttrd  8205  ltletrd  8503  le2addd  8643  le2subd  8644  ltleaddd  8645  leltaddd  8646  lt2subd  8648  ltmul12a  8940  lediv12a  8974  lemul12ad  9022  lemul12bd  9023  lt2halvesd  9292  uzind  9491  uztrn  9672  xrlttrd  9938  xrlelttrd  9939  xrltletrd  9940  xrletrd  9941  ixxss1  10033  ixxss2  10034  ixxss12  10035  zsupcllemex  10380  zssinfcl  10382  fldiv4p1lem1div2  10455  seqf1og  10673  faclbnd3  10895  abs3lemd  11556  xrbdtri  11631  modfsummod  11813  mertenslemi1  11890  sin01gt0  12117  cos01gt0  12118  sin02gt0  12119  dvds2subd  12182  dvds2addd  12184  dvdstrd  12185  bezoutlemstep  12362  mulgcd  12381  gcddvdslcm  12439  lcmgcdeq  12449  mulgcddvds  12460  rpmulgcd2  12461  rpdvds  12465  divgcdcoprmex  12468  rpexp  12519  phimullem  12591  eulerthlem1  12593  eulerthlemrprm  12595  eulerthlemth  12598  prmdiveq  12602  pythagtriplem4  12635  pcqmul  12670  pcgcd1  12695  pcadd  12707  pockthlem  12723  4sqlem16  12773  exmidunben  12841  mulgass  13539  lmtopcnp  14766  blin2  14948  xmetxp  15023  tgqioo  15071  cncfmptid  15113  negcncf  15121  limcimolemlt  15180  plyadd  15267  plymul  15268  sinq12gt0  15346  logdivlti  15397  mpodvdsmulf1o  15506  perfectlem1  15515  2sqlem5  15640  2sqlem8  15644