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  7349  ltbtwnnqq  7499  prarloclemarch2  7503  addlocprlemeqgt  7616  addnqprlemrl  7641  addnqprlemru  7642  mulnqprlemrl  7657  mulnqprlemru  7658  ltexprlemrl  7694  ltexprlemru  7696  addcanprleml  7698  addcanprlemu  7699  recexprlemloc  7715  recexprlem1ssu  7718  cauappcvgprlemladdfl  7739  caucvgprlemloc  7759  caucvgprprlemloccalc  7768  letrd  8167  lelttrd  8168  lttrd  8169  ltletrd  8467  le2addd  8607  le2subd  8608  ltleaddd  8609  leltaddd  8610  lt2subd  8612  ltmul12a  8904  lediv12a  8938  lemul12ad  8986  lemul12bd  8987  lt2halvesd  9256  uzind  9454  uztrn  9635  xrlttrd  9901  xrlelttrd  9902  xrltletrd  9903  xrletrd  9904  ixxss1  9996  ixxss2  9997  ixxss12  9998  zsupcllemex  10337  zssinfcl  10339  fldiv4p1lem1div2  10412  seqf1og  10630  faclbnd3  10852  abs3lemd  11383  xrbdtri  11458  modfsummod  11640  mertenslemi1  11717  sin01gt0  11944  cos01gt0  11945  sin02gt0  11946  dvds2subd  12009  dvds2addd  12011  dvdstrd  12012  bezoutlemstep  12189  mulgcd  12208  gcddvdslcm  12266  lcmgcdeq  12276  mulgcddvds  12287  rpmulgcd2  12288  rpdvds  12292  divgcdcoprmex  12295  rpexp  12346  phimullem  12418  eulerthlem1  12420  eulerthlemrprm  12422  eulerthlemth  12425  prmdiveq  12429  pythagtriplem4  12462  pcqmul  12497  pcgcd1  12522  pcadd  12534  pockthlem  12550  4sqlem16  12600  exmidunben  12668  mulgass  13365  lmtopcnp  14570  blin2  14752  xmetxp  14827  tgqioo  14875  cncfmptid  14917  negcncf  14925  limcimolemlt  14984  plyadd  15071  plymul  15072  sinq12gt0  15150  logdivlti  15201  mpodvdsmulf1o  15310  perfectlem1  15319  2sqlem5  15444  2sqlem8  15448