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  4679  tfr0dm  6474  tfr1onlemaccex  6500  tfrcllemaccex  6513  ertrd  6704  th3qlem1  6792  en2prd  6978  findcard2  7059  findcard2s  7060  diffifi  7064  fimax2gtrilemstep  7070  fidcenumlemrk  7129  fidcenumlemr  7130  isbth  7142  nninfninc  7298  cc2lem  7460  ltbtwnnqq  7610  prarloclemarch2  7614  addlocprlemeqgt  7727  addnqprlemrl  7752  addnqprlemru  7753  mulnqprlemrl  7768  mulnqprlemru  7769  ltexprlemrl  7805  ltexprlemru  7807  addcanprleml  7809  addcanprlemu  7810  recexprlemloc  7826  recexprlem1ssu  7829  cauappcvgprlemladdfl  7850  caucvgprlemloc  7870  caucvgprprlemloccalc  7879  letrd  8278  lelttrd  8279  lttrd  8280  ltletrd  8578  le2addd  8718  le2subd  8719  ltleaddd  8720  leltaddd  8721  lt2subd  8723  ltmul12a  9015  lediv12a  9049  lemul12ad  9097  lemul12bd  9098  lt2halvesd  9367  uzind  9566  uztrn  9747  xrlttrd  10013  xrlelttrd  10014  xrltletrd  10015  xrletrd  10016  ixxss1  10108  ixxss2  10109  ixxss12  10110  zsupcllemex  10458  zssinfcl  10460  fldiv4p1lem1div2  10533  seqf1og  10751  faclbnd3  10973  abs3lemd  11720  xrbdtri  11795  modfsummod  11977  mertenslemi1  12054  sin01gt0  12281  cos01gt0  12282  sin02gt0  12283  dvds2subd  12346  dvds2addd  12348  dvdstrd  12349  bezoutlemstep  12526  mulgcd  12545  gcddvdslcm  12603  lcmgcdeq  12613  mulgcddvds  12624  rpmulgcd2  12625  rpdvds  12629  divgcdcoprmex  12632  rpexp  12683  phimullem  12755  eulerthlem1  12757  eulerthlemrprm  12759  eulerthlemth  12762  prmdiveq  12766  pythagtriplem4  12799  pcqmul  12834  pcgcd1  12859  pcadd  12871  pockthlem  12887  4sqlem16  12937  exmidunben  13005  mulgass  13704  lmtopcnp  14932  blin2  15114  xmetxp  15189  tgqioo  15237  cncfmptid  15279  negcncf  15287  limcimolemlt  15346  plyadd  15433  plymul  15434  sinq12gt0  15512  logdivlti  15563  mpodvdsmulf1o  15672  perfectlem1  15681  2sqlem5  15806  2sqlem8  15810