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  4714  tfr0dm  6566  tfr1onlemaccex  6592  tfrcllemaccex  6605  ertrd  6796  th3qlem1  6884  en2prd  7072  findcard2  7159  findcard2s  7160  diffifi  7164  fimax2gtrilemstep  7171  fidcenumlemrk  7237  fidcenumlemr  7238  isbth  7250  nninfninc  7427  cc2lem  7596  ltbtwnnqq  7746  prarloclemarch2  7750  addlocprlemeqgt  7863  addnqprlemrl  7888  addnqprlemru  7889  mulnqprlemrl  7904  mulnqprlemru  7905  ltexprlemrl  7941  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  recexprlemloc  7962  recexprlem1ssu  7965  cauappcvgprlemladdfl  7986  caucvgprlemloc  8006  caucvgprprlemloccalc  8015  letrd  8414  lelttrd  8415  lttrd  8416  ltletrd  8715  le2addd  8855  le2subd  8856  ltleaddd  8857  leltaddd  8858  lt2subd  8860  ltmul12a  9154  lediv12a  9188  lemul12ad  9236  lemul12bd  9237  lt2halvesd  9506  uzind  9710  uztrn  9892  xrlttrd  10164  xrlelttrd  10165  xrltletrd  10166  xrletrd  10167  ixxss1  10259  ixxss2  10260  ixxss12  10261  zsupcllemex  10615  zssinfcl  10617  fldiv4p1lem1div2  10692  seqf1og  10910  faclbnd3  11133  abs3lemd  11914  xrbdtri  11989  modfsummod  12172  mertenslemi1  12249  sin01gt0  12476  cos01gt0  12477  sin02gt0  12478  dvds2subd  12541  dvds2addd  12543  dvdstrd  12544  bezoutlemstep  12721  mulgcd  12740  gcddvdslcm  12798  lcmgcdeq  12808  mulgcddvds  12819  rpmulgcd2  12820  rpdvds  12824  divgcdcoprmex  12827  rpexp  12878  phimullem  12950  eulerthlem1  12952  eulerthlemrprm  12954  eulerthlemth  12957  prmdiveq  12961  pythagtriplem4  12994  pcqmul  13029  pcgcd1  13054  pcadd  13066  pockthlem  13082  4sqlem16  13132  exmidunben  13264  mulgass  13915  lmtopcnp  15244  blin2  15426  xmetxp  15501  tgqioo  15549  cncfmptid  15591  negcncf  15599  limcimolemlt  15658  plyadd  15745  plymul  15746  sinq12gt0  15824  logdivlti  15875  mpodvdsmulf1o  15987  perfectlem1  15996  2sqlem5  16121  2sqlem8  16125