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  4687  tfr0dm  6493  tfr1onlemaccex  6519  tfrcllemaccex  6532  ertrd  6723  th3qlem1  6811  en2prd  6997  findcard2  7083  findcard2s  7084  diffifi  7088  fimax2gtrilemstep  7095  fidcenumlemrk  7158  fidcenumlemr  7159  isbth  7171  nninfninc  7327  cc2lem  7490  ltbtwnnqq  7640  prarloclemarch2  7644  addlocprlemeqgt  7757  addnqprlemrl  7782  addnqprlemru  7783  mulnqprlemrl  7798  mulnqprlemru  7799  ltexprlemrl  7835  ltexprlemru  7837  addcanprleml  7839  addcanprlemu  7840  recexprlemloc  7856  recexprlem1ssu  7859  cauappcvgprlemladdfl  7880  caucvgprlemloc  7900  caucvgprprlemloccalc  7909  letrd  8308  lelttrd  8309  lttrd  8310  ltletrd  8608  le2addd  8748  le2subd  8749  ltleaddd  8750  leltaddd  8751  lt2subd  8753  ltmul12a  9045  lediv12a  9079  lemul12ad  9127  lemul12bd  9128  lt2halvesd  9397  uzind  9596  uztrn  9778  xrlttrd  10049  xrlelttrd  10050  xrltletrd  10051  xrletrd  10052  ixxss1  10144  ixxss2  10145  ixxss12  10146  zsupcllemex  10496  zssinfcl  10498  fldiv4p1lem1div2  10571  seqf1og  10789  faclbnd3  11011  abs3lemd  11784  xrbdtri  11859  modfsummod  12042  mertenslemi1  12119  sin01gt0  12346  cos01gt0  12347  sin02gt0  12348  dvds2subd  12411  dvds2addd  12413  dvdstrd  12414  bezoutlemstep  12591  mulgcd  12610  gcddvdslcm  12668  lcmgcdeq  12678  mulgcddvds  12689  rpmulgcd2  12690  rpdvds  12694  divgcdcoprmex  12697  rpexp  12748  phimullem  12820  eulerthlem1  12822  eulerthlemrprm  12824  eulerthlemth  12827  prmdiveq  12831  pythagtriplem4  12864  pcqmul  12899  pcgcd1  12924  pcadd  12936  pockthlem  12952  4sqlem16  13002  exmidunben  13070  mulgass  13769  lmtopcnp  15003  blin2  15185  xmetxp  15260  tgqioo  15308  cncfmptid  15350  negcncf  15358  limcimolemlt  15417  plyadd  15504  plymul  15505  sinq12gt0  15583  logdivlti  15634  mpodvdsmulf1o  15743  perfectlem1  15752  2sqlem5  15877  2sqlem8  15881