Theorem mp2and 425

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  tfisi  4430  tfr0dm  6125  tfr1onlemaccex  6151  tfrcllemaccex  6164  ertrd  6348  th3qlem1  6434  findcard2  6685  findcard2s  6686  diffifi  6690  fimax2gtrilemstep  6696  fidcenumlemrk  6743  fidcenumlemr  6744  isbth  6756  ltbtwnnqq  7071  prarloclemarch2  7075  addlocprlemeqgt  7188  addnqprlemrl  7213  addnqprlemru  7214  mulnqprlemrl  7229  mulnqprlemru  7230  ltexprlemrl  7266  ltexprlemru  7268  addcanprleml  7270  addcanprlemu  7271  recexprlemloc  7287  recexprlem1ssu  7290  cauappcvgprlemladdfl  7311  caucvgprlemloc  7331  caucvgprprlemloccalc  7340  letrd  7704  lelttrd  7705  lttrd  7706  ltletrd  7998  le2addd  8137  le2subd  8138  ltleaddd  8139  leltaddd  8140  lt2subd  8142  ltmul12a  8418  lediv12a  8452  lemul12ad  8500  lemul12bd  8501  lt2halvesd  8761  uzind  8956  uztrn  9134  xrlttrd  9375  xrlelttrd  9376  xrltletrd  9377  xrletrd  9378  ixxss1  9470  ixxss2  9471  ixxss12  9472  fldiv4p1lem1div2  9861  faclbnd3  10266  abs3lemd  10749  xrbdtri  10819  modfsummod  11001  mertenslemi1  11078  sin01gt0  11201  cos01gt0  11202  sin02gt0  11203  dvds2subd  11259  zsupcllemex  11369  zssinfcl  11371  bezoutlemstep  11413  mulgcd  11432  gcddvdslcm  11482  lcmgcdeq  11492  mulgcddvds  11503  rpmulgcd2  11504  rpdvds  11508  divgcdcoprmex  11511  rpexp  11559  phimullem  11628  lmtopcnp  12101  blin2  12218  tgqioo  12323  cncfmptid  12349  negcncf  12353