Theorem mp2and 437

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 433	. 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  4732  tfr0dm  6587  tfr1onlemaccex  6613  tfrcllemaccex  6626  ertrd  6817  th3qlem1  6905  en2prd  7100  findcard2  7187  findcard2s  7188  diffifi  7192  fimax2gtrilemstep  7199  fidcenumlemrk  7265  fidcenumlemr  7266  isbth  7278  nninfninc  7457  cc2lem  7626  ltbtwnnqq  7776  prarloclemarch2  7780  addlocprlemeqgt  7893  addnqprlemrl  7918  addnqprlemru  7919  mulnqprlemrl  7934  mulnqprlemru  7935  ltexprlemrl  7971  ltexprlemru  7973  addcanprleml  7975  addcanprlemu  7976  recexprlemloc  7992  recexprlem1ssu  7995  cauappcvgprlemladdfl  8016  caucvgprlemloc  8036  caucvgprprlemloccalc  8045  letrd  8444  lelttrd  8445  lttrd  8446  ltletrd  8745  le2addd  8885  le2subd  8886  ltleaddd  8887  leltaddd  8888  lt2subd  8890  ltmul12a  9184  lediv12a  9218  lemul12ad  9266  lemul12bd  9267  lt2halvesd  9536  uzind  9740  uztrn  9922  xrlttrd  10194  xrlelttrd  10195  xrltletrd  10196  xrletrd  10197  ixxss1  10289  ixxss2  10290  ixxss12  10291  zsupcllemex  10646  zssinfcl  10648  fldiv4p1lem1div2  10723  seqf1og  10941  faclbnd3  11164  abs3lemd  11950  xrbdtri  12025  modfsummod  12208  mertenslemi1  12285  sin01gt0  12512  cos01gt0  12513  sin02gt0  12514  dvds2subd  12577  dvds2addd  12579  dvdstrd  12580  bezoutlemstep  12757  mulgcd  12776  gcddvdslcm  12834  lcmgcdeq  12844  mulgcddvds  12855  rpmulgcd2  12856  rpdvds  12860  divgcdcoprmex  12863  rpexp  12914  phimullem  12986  eulerthlem1  12988  eulerthlemrprm  12990  eulerthlemth  12993  prmdiveq  12997  pythagtriplem4  13030  pcqmul  13065  pcgcd1  13090  pcadd  13102  pockthlem  13118  4sqlem16  13168  exmidunben  13300  mulgass  13945  lmtopcnp  15334  blin2  15516  xmetxp  15591  tgqioo  15639  cncfmptid  15681  negcncf  15689  limcimolemlt  15748  plyadd  15835  plymul  15836  sinq12gt0  15914  logdivlti  15965  mpodvdsmulf1o  16087  perfectlem1  16096  2sqlem5  16221  2sqlem8  16225