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  6389  tfr1onlemaccex  6415  tfrcllemaccex  6428  ertrd  6617  th3qlem1  6705  findcard2  6959  findcard2s  6960  diffifi  6964  fimax2gtrilemstep  6970  fidcenumlemrk  7029  fidcenumlemr  7030  isbth  7042  nninfninc  7198  cc2lem  7351  ltbtwnnqq  7501  prarloclemarch2  7505  addlocprlemeqgt  7618  addnqprlemrl  7643  addnqprlemru  7644  mulnqprlemrl  7659  mulnqprlemru  7660  ltexprlemrl  7696  ltexprlemru  7698  addcanprleml  7700  addcanprlemu  7701  recexprlemloc  7717  recexprlem1ssu  7720  cauappcvgprlemladdfl  7741  caucvgprlemloc  7761  caucvgprprlemloccalc  7770  letrd  8169  lelttrd  8170  lttrd  8171  ltletrd  8469  le2addd  8609  le2subd  8610  ltleaddd  8611  leltaddd  8612  lt2subd  8614  ltmul12a  8906  lediv12a  8940  lemul12ad  8988  lemul12bd  8989  lt2halvesd  9258  uzind  9456  uztrn  9637  xrlttrd  9903  xrlelttrd  9904  xrltletrd  9905  xrletrd  9906  ixxss1  9998  ixxss2  9999  ixxss12  10000  zsupcllemex  10339  zssinfcl  10341  fldiv4p1lem1div2  10414  seqf1og  10632  faclbnd3  10854  abs3lemd  11385  xrbdtri  11460  modfsummod  11642  mertenslemi1  11719  sin01gt0  11946  cos01gt0  11947  sin02gt0  11948  dvds2subd  12011  dvds2addd  12013  dvdstrd  12014  bezoutlemstep  12191  mulgcd  12210  gcddvdslcm  12268  lcmgcdeq  12278  mulgcddvds  12289  rpmulgcd2  12290  rpdvds  12294  divgcdcoprmex  12297  rpexp  12348  phimullem  12420  eulerthlem1  12422  eulerthlemrprm  12424  eulerthlemth  12427  prmdiveq  12431  pythagtriplem4  12464  pcqmul  12499  pcgcd1  12524  pcadd  12536  pockthlem  12552  4sqlem16  12602  exmidunben  12670  mulgass  13367  lmtopcnp  14572  blin2  14754  xmetxp  14829  tgqioo  14877  cncfmptid  14919  negcncf  14927  limcimolemlt  14986  plyadd  15073  plymul  15074  sinq12gt0  15152  logdivlti  15203  mpodvdsmulf1o  15312  perfectlem1  15321  2sqlem5  15446  2sqlem8  15450