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  7958  muladd11  8461  negsub  8576  subneg  8577  ltaddneg  8754  muleqadd  9001  diveqap1  9038  conjmulap  9062  nnsub  9346  addltmul  9547  zltp1le  9704  gtndiv  9746  eluzp1m1  9956  xnn0le2is012  10279  divelunit  10415  fznatpl1  10494  flqbi2  10741  flqdiv  10773  frecfzen2  10879  nn0ennn  10885  seqshft2g  10934  seqf1oglem1  10971  faclbnd3  11197  ccatrid  11391  shftfvalg  11599  ovshftex  11600  shftfval  11602  abs2dif  11889  cos2t  12536  sin01gt0  12548  cos01gt0  12549  demoivre  12559  demoivreALT  12560  omeo  12684  gcd0id  12775  sqgcd  12825  isprm3  12915  eulerthlemth  13033  pczpre  13099  pcrec  13110  setscom  13444  setsslid  13455  setsslnid  13456  mulgm1  13998  abssinper  16039  ppiqub  16254  chtqub  16257  bposlem2  16273  lgs1  16329