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  4620  tfr0dm  6377  tfr1onlemaccex  6403  tfrcllemaccex  6416  ertrd  6605  th3qlem1  6693  findcard2  6947  findcard2s  6948  diffifi  6952  fimax2gtrilemstep  6958  fidcenumlemrk  7015  fidcenumlemr  7016  isbth  7028  nninfninc  7184  cc2lem  7328  ltbtwnnqq  7477  prarloclemarch2  7481  addlocprlemeqgt  7594  addnqprlemrl  7619  addnqprlemru  7620  mulnqprlemrl  7635  mulnqprlemru  7636  ltexprlemrl  7672  ltexprlemru  7674  addcanprleml  7676  addcanprlemu  7677  recexprlemloc  7693  recexprlem1ssu  7696  cauappcvgprlemladdfl  7717  caucvgprlemloc  7737  caucvgprprlemloccalc  7746  letrd  8145  lelttrd  8146  lttrd  8147  ltletrd  8444  le2addd  8584  le2subd  8585  ltleaddd  8586  leltaddd  8587  lt2subd  8589  ltmul12a  8881  lediv12a  8915  lemul12ad  8963  lemul12bd  8964  lt2halvesd  9233  uzind  9431  uztrn  9612  xrlttrd  9878  xrlelttrd  9879  xrltletrd  9880  xrletrd  9881  ixxss1  9973  ixxss2  9974  ixxss12  9975  fldiv4p1lem1div2  10377  seqf1og  10595  faclbnd3  10817  abs3lemd  11348  xrbdtri  11422  modfsummod  11604  mertenslemi1  11681  sin01gt0  11908  cos01gt0  11909  sin02gt0  11910  dvds2subd  11973  dvds2addd  11975  dvdstrd  11976  zsupcllemex  12086  zssinfcl  12088  bezoutlemstep  12137  mulgcd  12156  gcddvdslcm  12214  lcmgcdeq  12224  mulgcddvds  12235  rpmulgcd2  12236  rpdvds  12240  divgcdcoprmex  12243  rpexp  12294  phimullem  12366  eulerthlem1  12368  eulerthlemrprm  12370  eulerthlemth  12373  prmdiveq  12377  pythagtriplem4  12409  pcqmul  12444  pcgcd1  12469  pcadd  12481  pockthlem  12497  4sqlem16  12547  exmidunben  12586  mulgass  13232  lmtopcnp  14429  blin2  14611  xmetxp  14686  tgqioo  14734  cncfmptid  14776  negcncf  14784  limcimolemlt  14843  plyadd  14930  plymul  14931  sinq12gt0  15006  logdivlti  15057  2sqlem5  15276  2sqlem8  15280