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  4624  tfr0dm  6381  tfr1onlemaccex  6407  tfrcllemaccex  6420  ertrd  6609  th3qlem1  6697  findcard2  6951  findcard2s  6952  diffifi  6956  fimax2gtrilemstep  6962  fidcenumlemrk  7021  fidcenumlemr  7022  isbth  7034  nninfninc  7190  cc2lem  7335  ltbtwnnqq  7484  prarloclemarch2  7488  addlocprlemeqgt  7601  addnqprlemrl  7626  addnqprlemru  7627  mulnqprlemrl  7642  mulnqprlemru  7643  ltexprlemrl  7679  ltexprlemru  7681  addcanprleml  7683  addcanprlemu  7684  recexprlemloc  7700  recexprlem1ssu  7703  cauappcvgprlemladdfl  7724  caucvgprlemloc  7744  caucvgprprlemloccalc  7753  letrd  8152  lelttrd  8153  lttrd  8154  ltletrd  8452  le2addd  8592  le2subd  8593  ltleaddd  8594  leltaddd  8595  lt2subd  8597  ltmul12a  8889  lediv12a  8923  lemul12ad  8971  lemul12bd  8972  lt2halvesd  9241  uzind  9439  uztrn  9620  xrlttrd  9886  xrlelttrd  9887  xrltletrd  9888  xrletrd  9889  ixxss1  9981  ixxss2  9982  ixxss12  9983  zsupcllemex  10322  zssinfcl  10324  fldiv4p1lem1div2  10397  seqf1og  10615  faclbnd3  10837  abs3lemd  11368  xrbdtri  11443  modfsummod  11625  mertenslemi1  11702  sin01gt0  11929  cos01gt0  11930  sin02gt0  11931  dvds2subd  11994  dvds2addd  11996  dvdstrd  11997  bezoutlemstep  12174  mulgcd  12193  gcddvdslcm  12251  lcmgcdeq  12261  mulgcddvds  12272  rpmulgcd2  12273  rpdvds  12277  divgcdcoprmex  12280  rpexp  12331  phimullem  12403  eulerthlem1  12405  eulerthlemrprm  12407  eulerthlemth  12410  prmdiveq  12414  pythagtriplem4  12447  pcqmul  12482  pcgcd1  12507  pcadd  12519  pockthlem  12535  4sqlem16  12585  exmidunben  12653  mulgass  13299  lmtopcnp  14496  blin2  14678  xmetxp  14753  tgqioo  14801  cncfmptid  14843  negcncf  14851  limcimolemlt  14910  plyadd  14997  plymul  14998  sinq12gt0  15076  logdivlti  15127  mpodvdsmulf1o  15236  perfectlem1  15245  2sqlem5  15370  2sqlem8  15374