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  4587  tfr0dm  6323  tfr1onlemaccex  6349  tfrcllemaccex  6362  ertrd  6551  th3qlem1  6637  findcard2  6889  findcard2s  6890  diffifi  6894  fimax2gtrilemstep  6900  fidcenumlemrk  6953  fidcenumlemr  6954  isbth  6966  cc2lem  7265  ltbtwnnqq  7414  prarloclemarch2  7418  addlocprlemeqgt  7531  addnqprlemrl  7556  addnqprlemru  7557  mulnqprlemrl  7572  mulnqprlemru  7573  ltexprlemrl  7609  ltexprlemru  7611  addcanprleml  7613  addcanprlemu  7614  recexprlemloc  7630  recexprlem1ssu  7633  cauappcvgprlemladdfl  7654  caucvgprlemloc  7674  caucvgprprlemloccalc  7683  letrd  8081  lelttrd  8082  lttrd  8083  ltletrd  8380  le2addd  8520  le2subd  8521  ltleaddd  8522  leltaddd  8523  lt2subd  8525  ltmul12a  8817  lediv12a  8851  lemul12ad  8899  lemul12bd  8900  lt2halvesd  9166  uzind  9364  uztrn  9544  xrlttrd  9809  xrlelttrd  9810  xrltletrd  9811  xrletrd  9812  ixxss1  9904  ixxss2  9905  ixxss12  9906  fldiv4p1lem1div2  10305  faclbnd3  10723  abs3lemd  11210  xrbdtri  11284  modfsummod  11466  mertenslemi1  11543  sin01gt0  11769  cos01gt0  11770  sin02gt0  11771  dvds2subd  11834  dvds2addd  11836  dvdstrd  11837  zsupcllemex  11947  zssinfcl  11949  bezoutlemstep  11998  mulgcd  12017  gcddvdslcm  12073  lcmgcdeq  12083  mulgcddvds  12094  rpmulgcd2  12095  rpdvds  12099  divgcdcoprmex  12102  rpexp  12153  phimullem  12225  eulerthlem1  12227  eulerthlemrprm  12229  eulerthlemth  12232  prmdiveq  12236  pythagtriplem4  12268  pcqmul  12303  pcgcd1  12327  pcadd  12339  pockthlem  12354  exmidunben  12427  mulgass  13020  lmtopcnp  13753  blin2  13935  xmetxp  14010  tgqioo  14050  cncfmptid  14086  negcncf  14091  limcimolemlt  14136  sinq12gt0  14254  logdivlti  14305  2sqlem5  14469  2sqlem8  14473