Theorem mp3an2 1220

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 1104	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 411	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885

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

This theorem is referenced by:  mp3anl2  1227  ordin  4122  ordsuc  4287  omv  6035  oeiv  6036  omv2  6045  1idprl  6688  muladd11  7146  negsub  7259  subneg  7260  muleqadd  7649  diveqap1  7682  conjmulap  7705  nnsub  7952  addltmul  8161  zltp1le  8298  gtndiv  8335  eluzp1m1  8496  divelunit  8870  fznatpl1  8938  flqbi2  9133  flqdiv  9163  frecfzen2  9204  nn0ennn  9209  iseqshft2  9232  shftfvalg  9419  ovshftex  9420  shftfval  9422  abs2dif  9702