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 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1009

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

This theorem is referenced by:  mp3anl2  1373  ordin  4525  ordsuc  4705  omv  6718  oeiv  6719  omv2  6728  1idprl  7947  muladd11  8449  negsub  8564  subneg  8565  ltaddneg  8742  muleqadd  8988  diveqap1  9025  conjmulap  9049  nnsub  9322  addltmul  9521  zltp1le  9678  gtndiv  9720  eluzp1m1  9925  xnn0le2is012  10247  divelunit  10383  fznatpl1  10461  flqbi2  10704  flqdiv  10736  frecfzen2  10842  nn0ennn  10848  seqshft2g  10897  seqf1oglem1  10934  faclbnd3  11159  ccatrid  11353  shftfvalg  11561  ovshftex  11562  shftfval  11564  abs2dif  11850  cos2t  12495  sin01gt0  12507  cos01gt0  12508  demoivre  12518  demoivreALT  12519  omeo  12643  gcd0id  12734  sqgcd  12784  isprm3  12874  eulerthlemth  12988  pczpre  13054  pcrec  13065  setscom  13370  setsslid  13381  setsslnid  13382  mulgm1  13922  abssinper  15870  lgs1  16077