Theorem mp3an2 1366

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an2.1	⊢ 𝜓
mp3an2.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an2	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mp3an2

Step	Hyp	Ref	Expression
1		mp3an2.1	. 2 ⊢ 𝜓
2		mp3an2.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expa 1234	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 439	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

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

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  df-3an 1011

This theorem is used by:  mp3anl2  1373  ordin  4530  ordsuc  4710  omv  6728  oeiv  6729  omv2  6738  1idprl  7957  muladd11  8459  negsub  8574  subneg  8575  ltaddneg  8752  muleqadd  8998  diveqap1  9035  conjmulap  9059  nnsub  9343  addltmul  9542  zltp1le  9699  gtndiv  9741  eluzp1m1  9946  xnn0le2is012  10268  divelunit  10404  fznatpl1  10483  flqbi2  10726  flqdiv  10758  frecfzen2  10864  nn0ennn  10870  seqshft2g  10919  seqf1oglem1  10956  faclbnd3  11181  ccatrid  11375  shftfvalg  11583  ovshftex  11584  shftfval  11586  abs2dif  11872  cos2t  12517  sin01gt0  12529  cos01gt0  12530  demoivre  12540  demoivreALT  12541  omeo  12665  gcd0id  12756  sqgcd  12806  isprm3  12896  eulerthlemth  13010  pczpre  13076  pcrec  13087  setscom  13392  setsslid  13403  setsslnid  13404  mulgm1  13945  abssinper  15947  lgs1  16163