Theorem mp2and 429

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 425	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5	1, 4	mpd 13	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  tfisi  4501  tfr0dm  6219  tfr1onlemaccex  6245  tfrcllemaccex  6258  ertrd  6445  th3qlem1  6531  findcard2  6783  findcard2s  6784  diffifi  6788  fimax2gtrilemstep  6794  fidcenumlemrk  6842  fidcenumlemr  6843  isbth  6855  ltbtwnnqq  7223  prarloclemarch2  7227  addlocprlemeqgt  7340  addnqprlemrl  7365  addnqprlemru  7366  mulnqprlemrl  7381  mulnqprlemru  7382  ltexprlemrl  7418  ltexprlemru  7420  addcanprleml  7422  addcanprlemu  7423  recexprlemloc  7439  recexprlem1ssu  7442  cauappcvgprlemladdfl  7463  caucvgprlemloc  7483  caucvgprprlemloccalc  7492  letrd  7886  lelttrd  7887  lttrd  7888  ltletrd  8185  le2addd  8325  le2subd  8326  ltleaddd  8327  leltaddd  8328  lt2subd  8330  ltmul12a  8618  lediv12a  8652  lemul12ad  8700  lemul12bd  8701  lt2halvesd  8967  uzind  9162  uztrn  9342  xrlttrd  9592  xrlelttrd  9593  xrltletrd  9594  xrletrd  9595  ixxss1  9687  ixxss2  9688  ixxss12  9689  fldiv4p1lem1div2  10078  faclbnd3  10489  abs3lemd  10973  xrbdtri  11045  modfsummod  11227  mertenslemi1  11304  sin01gt0  11468  cos01gt0  11469  sin02gt0  11470  dvds2subd  11529  zsupcllemex  11639  zssinfcl  11641  bezoutlemstep  11685  mulgcd  11704  gcddvdslcm  11754  lcmgcdeq  11764  mulgcddvds  11775  rpmulgcd2  11776  rpdvds  11780  divgcdcoprmex  11783  rpexp  11831  phimullem  11901  exmidunben  11939  lmtopcnp  12419  blin2  12601  xmetxp  12676  tgqioo  12716  cncfmptid  12752  negcncf  12757  limcimolemlt  12802  sinq12gt0  12911