Theorem mp2and 430

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 426	. 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  4509  tfr0dm  6227  tfr1onlemaccex  6253  tfrcllemaccex  6266  ertrd  6453  th3qlem1  6539  findcard2  6791  findcard2s  6792  diffifi  6796  fimax2gtrilemstep  6802  fidcenumlemrk  6850  fidcenumlemr  6851  isbth  6863  cc2lem  7098  ltbtwnnqq  7247  prarloclemarch2  7251  addlocprlemeqgt  7364  addnqprlemrl  7389  addnqprlemru  7390  mulnqprlemrl  7405  mulnqprlemru  7406  ltexprlemrl  7442  ltexprlemru  7444  addcanprleml  7446  addcanprlemu  7447  recexprlemloc  7463  recexprlem1ssu  7466  cauappcvgprlemladdfl  7487  caucvgprlemloc  7507  caucvgprprlemloccalc  7516  letrd  7910  lelttrd  7911  lttrd  7912  ltletrd  8209  le2addd  8349  le2subd  8350  ltleaddd  8351  leltaddd  8352  lt2subd  8354  ltmul12a  8642  lediv12a  8676  lemul12ad  8724  lemul12bd  8725  lt2halvesd  8991  uzind  9186  uztrn  9366  xrlttrd  9622  xrlelttrd  9623  xrltletrd  9624  xrletrd  9625  ixxss1  9717  ixxss2  9718  ixxss12  9719  fldiv4p1lem1div2  10109  faclbnd3  10521  abs3lemd  11005  xrbdtri  11077  modfsummod  11259  mertenslemi1  11336  sin01gt0  11504  cos01gt0  11505  sin02gt0  11506  dvds2subd  11565  zsupcllemex  11675  zssinfcl  11677  bezoutlemstep  11721  mulgcd  11740  gcddvdslcm  11790  lcmgcdeq  11800  mulgcddvds  11811  rpmulgcd2  11812  rpdvds  11816  divgcdcoprmex  11819  rpexp  11867  phimullem  11937  exmidunben  11975  lmtopcnp  12458  blin2  12640  xmetxp  12715  tgqioo  12755  cncfmptid  12791  negcncf  12796  limcimolemlt  12841  sinq12gt0  12959  logdivlti  13010