Theorem mp2and 423

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

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  tfisi  4328  tfr0  5960  ertrd  6145  th3qlem1  6231  findcard2  6373  findcard2s  6374  diffifi  6378  ltbtwnnqq  6605  prarloclemarch2  6609  addlocprlemeqgt  6722  addnqprlemrl  6747  addnqprlemru  6748  mulnqprlemrl  6763  mulnqprlemru  6764  ltexprlemrl  6800  ltexprlemru  6802  addcanprleml  6804  addcanprlemu  6805  recexprlemloc  6821  recexprlem1ssu  6824  cauappcvgprlemladdfl  6845  caucvgprlemloc  6865  caucvgprprlemloccalc  6874  letrd  7233  lelttrd  7234  lttrd  7235  ltletrd  7527  le2addd  7663  le2subd  7664  ltleaddd  7665  leltaddd  7666  lt2subd  7668  ltmul12a  7938  lediv12a  7972  lemul12ad  8020  lemul12bd  8021  lt2halvesd  8278  uzind  8458  uztrn  8635  xrlttrd  8879  xrlelttrd  8880  xrltletrd  8881  xrletrd  8882  ixxss1  8927  ixxss2  8928  ixxss12  8929  fldiv4p1lem1div2  9307  faclbnd3  9670  abs3lemd  10087  dvds2subd  10231  zsupcllemex  10342  zssinfcl  10344  bezoutlemstep  10386  mulgcd  10405  gcddvdslcm  10455  lcmgcdeq  10465  mulgcddvds  10476  rpmulgcd2  10477  rpdvds  10481  divgcdcoprmex  10484  rpexp  10532