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  4619  tfr0dm  6375  tfr1onlemaccex  6401  tfrcllemaccex  6414  ertrd  6603  th3qlem1  6691  findcard2  6945  findcard2s  6946  diffifi  6950  fimax2gtrilemstep  6956  fidcenumlemrk  7013  fidcenumlemr  7014  isbth  7026  nninfninc  7182  cc2lem  7326  ltbtwnnqq  7475  prarloclemarch2  7479  addlocprlemeqgt  7592  addnqprlemrl  7617  addnqprlemru  7618  mulnqprlemrl  7633  mulnqprlemru  7634  ltexprlemrl  7670  ltexprlemru  7672  addcanprleml  7674  addcanprlemu  7675  recexprlemloc  7691  recexprlem1ssu  7694  cauappcvgprlemladdfl  7715  caucvgprlemloc  7735  caucvgprprlemloccalc  7744  letrd  8143  lelttrd  8144  lttrd  8145  ltletrd  8442  le2addd  8582  le2subd  8583  ltleaddd  8584  leltaddd  8585  lt2subd  8587  ltmul12a  8879  lediv12a  8913  lemul12ad  8961  lemul12bd  8962  lt2halvesd  9230  uzind  9428  uztrn  9609  xrlttrd  9875  xrlelttrd  9876  xrltletrd  9877  xrletrd  9878  ixxss1  9970  ixxss2  9971  ixxss12  9972  fldiv4p1lem1div2  10374  seqf1og  10592  faclbnd3  10814  abs3lemd  11345  xrbdtri  11419  modfsummod  11601  mertenslemi1  11678  sin01gt0  11905  cos01gt0  11906  sin02gt0  11907  dvds2subd  11970  dvds2addd  11972  dvdstrd  11973  zsupcllemex  12083  zssinfcl  12085  bezoutlemstep  12134  mulgcd  12153  gcddvdslcm  12211  lcmgcdeq  12221  mulgcddvds  12232  rpmulgcd2  12233  rpdvds  12237  divgcdcoprmex  12240  rpexp  12291  phimullem  12363  eulerthlem1  12365  eulerthlemrprm  12367  eulerthlemth  12370  prmdiveq  12374  pythagtriplem4  12406  pcqmul  12441  pcgcd1  12466  pcadd  12478  pockthlem  12494  4sqlem16  12544  exmidunben  12583  mulgass  13229  lmtopcnp  14418  blin2  14600  xmetxp  14675  tgqioo  14715  cncfmptid  14751  negcncf  14759  limcimolemlt  14818  plyadd  14897  plymul  14898  sinq12gt0  14965  logdivlti  15016  2sqlem5  15206  2sqlem8  15210