Theorem mp2and 433

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 429	. 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  4586  tfr0dm  6322  tfr1onlemaccex  6348  tfrcllemaccex  6361  ertrd  6550  th3qlem1  6636  findcard2  6888  findcard2s  6889  diffifi  6893  fimax2gtrilemstep  6899  fidcenumlemrk  6952  fidcenumlemr  6953  isbth  6965  cc2lem  7264  ltbtwnnqq  7413  prarloclemarch2  7417  addlocprlemeqgt  7530  addnqprlemrl  7555  addnqprlemru  7556  mulnqprlemrl  7571  mulnqprlemru  7572  ltexprlemrl  7608  ltexprlemru  7610  addcanprleml  7612  addcanprlemu  7613  recexprlemloc  7629  recexprlem1ssu  7632  cauappcvgprlemladdfl  7653  caucvgprlemloc  7673  caucvgprprlemloccalc  7682  letrd  8080  lelttrd  8081  lttrd  8082  ltletrd  8379  le2addd  8519  le2subd  8520  ltleaddd  8521  leltaddd  8522  lt2subd  8524  ltmul12a  8816  lediv12a  8850  lemul12ad  8898  lemul12bd  8899  lt2halvesd  9165  uzind  9363  uztrn  9543  xrlttrd  9808  xrlelttrd  9809  xrltletrd  9810  xrletrd  9811  ixxss1  9903  ixxss2  9904  ixxss12  9905  fldiv4p1lem1div2  10304  faclbnd3  10722  abs3lemd  11209  xrbdtri  11283  modfsummod  11465  mertenslemi1  11542  sin01gt0  11768  cos01gt0  11769  sin02gt0  11770  dvds2subd  11833  dvds2addd  11835  dvdstrd  11836  zsupcllemex  11946  zssinfcl  11948  bezoutlemstep  11997  mulgcd  12016  gcddvdslcm  12072  lcmgcdeq  12082  mulgcddvds  12093  rpmulgcd2  12094  rpdvds  12098  divgcdcoprmex  12101  rpexp  12152  phimullem  12224  eulerthlem1  12226  eulerthlemrprm  12228  eulerthlemth  12231  prmdiveq  12235  pythagtriplem4  12267  pcqmul  12302  pcgcd1  12326  pcadd  12338  pockthlem  12353  exmidunben  12426  mulgass  13018  lmtopcnp  13720  blin2  13902  xmetxp  13977  tgqioo  14017  cncfmptid  14053  negcncf  14058  limcimolemlt  14103  sinq12gt0  14221  logdivlti  14272  2sqlem5  14436  2sqlem8  14440