Theorem mp2and 437

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 433	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5	1, 4	mpd 13	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  tfisi  4734  tfr0dm  6593  tfr1onlemaccex  6619  tfrcllemaccex  6632  ertrd  6823  th3qlem1  6911  en2prd  7106  findcard2  7193  findcard2s  7194  diffifi  7198  fimax2gtrilemstep  7205  fidcenumlemrk  7271  fidcenumlemr  7272  isbth  7284  nninfninc  7463  cc2lem  7632  ltbtwnnqq  7782  prarloclemarch2  7786  addlocprlemeqgt  7899  addnqprlemrl  7924  addnqprlemru  7925  mulnqprlemrl  7940  mulnqprlemru  7941  ltexprlemrl  7977  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  recexprlemloc  7998  recexprlem1ssu  8001  cauappcvgprlemladdfl  8022  caucvgprlemloc  8042  caucvgprprlemloccalc  8051  letrd  8450  lelttrd  8451  lttrd  8452  ltletrd  8751  le2addd  8892  le2subd  8893  ltleaddd  8894  leltaddd  8895  lt2subd  8897  ltmul12a  9191  lediv12a  9225  lemul12ad  9273  lemul12bd  9274  lt2halvesd  9555  uzind  9759  uztrn  9941  xrlttrd  10213  xrlelttrd  10214  xrltletrd  10215  xrletrd  10216  ixxss1  10308  ixxss2  10309  ixxss12  10310  zsupcllemex  10665  zssinfcl  10667  fldiv4p1lem1div2  10742  seqf1og  10960  faclbnd3  11183  abs3lemd  11969  xrbdtri  12044  modfsummod  12227  mertenslemi1  12304  sin01gt0  12531  cos01gt0  12532  sin02gt0  12533  dvds2subd  12596  dvds2addd  12598  dvdstrd  12599  bezoutlemstep  12776  mulgcd  12795  gcddvdslcm  12853  lcmgcdeq  12863  mulgcddvds  12874  rpmulgcd2  12875  rpdvds  12879  divgcdcoprmex  12882  rpexp  12933  phimullem  13005  eulerthlem1  13007  eulerthlemrprm  13009  eulerthlemth  13012  prmdiveq  13016  pythagtriplem4  13049  pcqmul  13084  pcgcd1  13109  pcadd  13121  pockthlem  13137  4sqlem16  13187  exmidunben  13319  mulgass  13964  lmtopcnp  15353  blin2  15535  xmetxp  15610  tgqioo  15658  cncfmptid  15700  negcncf  15708  limcimolemlt  15767  plyadd  15854  plymul  15855  sinq12gt0  15934  logdivlti  15986  mpodvdsmulf1o  16110  perfectlem1  16119  2sqlem5  16250  2sqlem8  16254