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 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  tfisi  4734  tfr0dm  6593  tfr1onlemaccex  6619  tfrcllemaccex  6632  ertrd  6823  th3qlem1  6911  en2prd  7106  findcard2  7193  findcard2s  7194  diffifi  7198  fimax2gtrilemstep  7205  fidcenumlemrk  7271  fidcenumlemr  7272  isbth  7284  nninfninc  7463  cc2lem  7632  ltbtwnnqq  7782  prarloclemarch2  7786  addlocprlemeqgt  7899  addnqprlemrl  7924  addnqprlemru  7925  mulnqprlemrl  7940  mulnqprlemru  7941  ltexprlemrl  7977  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  recexprlemloc  7998  recexprlem1ssu  8001  cauappcvgprlemladdfl  8022  caucvgprlemloc  8042  caucvgprprlemloccalc  8051  letrd  8451  lelttrd  8452  lttrd  8453  ltletrd  8752  le2addd  8893  le2subd  8894  ltleaddd  8895  leltaddd  8896  lt2subd  8898  ltmul12a  9192  lediv12a  9226  lemul12ad  9274  lemul12bd  9275  lt2halvesd  9557  uzind  9761  uztrn  9948  xrlttrd  10221  xrlelttrd  10222  xrltletrd  10223  xrletrd  10224  ixxss1  10316  ixxss2  10317  ixxss12  10318  zsupcllemex  10673  zssinfcl  10675  fldiv4p1lem1div2  10753  seqf1og  10971  faclbnd3  11195  abs3lemd  11982  xrbdtri  12058  modfsummod  12241  mertenslemi1  12318  sin01gt0  12545  cos01gt0  12546  sin02gt0  12547  dvds2subd  12610  dvds2addd  12612  dvdstrd  12613  bezoutlemstep  12790  mulgcd  12809  gcddvdslcm  12867  lcmgcdeq  12877  mulgcddvds  12888  rpmulgcd2  12889  rpdvds  12893  divgcdcoprmex  12896  rpexp  12948  phimullem  13023  eulerthlem1  13025  eulerthlemrprm  13027  eulerthlemth  13030  prmdiveq  13034  pythagtriplem4  13067  pcqmul  13102  pcgcd1  13127  pcadd  13139  pockthlem  13155  4sqlem16  13205  exmidunben  13366  mulgass  14011  lmtopcnp  15400  blin2  15582  xmetxp  15657  tgqioo  15705  cncfmptid  15747  negcncf  15755  limcimolemlt  15814  plyadd  15901  plymul  15902  sinq12gt0  15981  logdivlti  16033  ppiprm  16178  mpodvdsmulf1o  16203  perfectlem1  16218  2sqlem5  16357  2sqlem8  16361