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  4656  tfr0dm  6438  tfr1onlemaccex  6464  tfrcllemaccex  6477  ertrd  6666  th3qlem1  6754  en2prd  6940  findcard2  7019  findcard2s  7020  diffifi  7024  fimax2gtrilemstep  7030  fidcenumlemrk  7089  fidcenumlemr  7090  isbth  7102  nninfninc  7258  cc2lem  7420  ltbtwnnqq  7570  prarloclemarch2  7574  addlocprlemeqgt  7687  addnqprlemrl  7712  addnqprlemru  7713  mulnqprlemrl  7728  mulnqprlemru  7729  ltexprlemrl  7765  ltexprlemru  7767  addcanprleml  7769  addcanprlemu  7770  recexprlemloc  7786  recexprlem1ssu  7789  cauappcvgprlemladdfl  7810  caucvgprlemloc  7830  caucvgprprlemloccalc  7839  letrd  8238  lelttrd  8239  lttrd  8240  ltletrd  8538  le2addd  8678  le2subd  8679  ltleaddd  8680  leltaddd  8681  lt2subd  8683  ltmul12a  8975  lediv12a  9009  lemul12ad  9057  lemul12bd  9058  lt2halvesd  9327  uzind  9526  uztrn  9707  xrlttrd  9973  xrlelttrd  9974  xrltletrd  9975  xrletrd  9976  ixxss1  10068  ixxss2  10069  ixxss12  10070  zsupcllemex  10417  zssinfcl  10419  fldiv4p1lem1div2  10492  seqf1og  10710  faclbnd3  10932  abs3lemd  11678  xrbdtri  11753  modfsummod  11935  mertenslemi1  12012  sin01gt0  12239  cos01gt0  12240  sin02gt0  12241  dvds2subd  12304  dvds2addd  12306  dvdstrd  12307  bezoutlemstep  12484  mulgcd  12503  gcddvdslcm  12561  lcmgcdeq  12571  mulgcddvds  12582  rpmulgcd2  12583  rpdvds  12587  divgcdcoprmex  12590  rpexp  12641  phimullem  12713  eulerthlem1  12715  eulerthlemrprm  12717  eulerthlemth  12720  prmdiveq  12724  pythagtriplem4  12757  pcqmul  12792  pcgcd1  12817  pcadd  12829  pockthlem  12845  4sqlem16  12895  exmidunben  12963  mulgass  13662  lmtopcnp  14889  blin2  15071  xmetxp  15146  tgqioo  15194  cncfmptid  15236  negcncf  15244  limcimolemlt  15303  plyadd  15390  plymul  15391  sinq12gt0  15469  logdivlti  15520  mpodvdsmulf1o  15629  perfectlem1  15638  2sqlem5  15763  2sqlem8  15767