Theorem mp2and 409

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

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  ssnelpssd  3290  tfisi  4310  tfr0  5937  ertrd  6122  th3qlem1  6208  findcard2  6346  findcard2s  6347  diffifi  6351  ltbtwnnqq  6513  prarloclemarch2  6517  addlocprlemeqgt  6630  addnqprlemrl  6655  addnqprlemru  6656  mulnqprlemrl  6671  mulnqprlemru  6672  ltexprlemrl  6708  ltexprlemru  6710  addcanprleml  6712  addcanprlemu  6713  recexprlemloc  6729  recexprlem1ssu  6732  cauappcvgprlemladdfl  6753  caucvgprlemloc  6773  caucvgprprlemloccalc  6782  letrd  7138  lelttrd  7139  lttrd  7140  ltletrd  7420  le2addd  7554  le2subd  7555  ltleaddd  7556  leltaddd  7557  lt2subd  7559  ltmul12a  7826  lediv12a  7860  lemul12ad  7908  lemul12bd  7909  lt2halvesd  8172  uzind  8349  uztrn  8489  xrlttrd  8725  xrlelttrd  8726  xrltletrd  8727  xrletrd  8728  ixxss1  8773  ixxss2  8774  ixxss12  8775  fldiv4p1lem1div2  9147  abs3lemd  9797