Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  jaoian Structured version   Visualization version   GIF version

Theorem jaoian 954
 Description: Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.)
Hypotheses
Ref Expression
jaoian.1 ((𝜑𝜓) → 𝜒)
jaoian.2 ((𝜃𝜓) → 𝜒)
Assertion
Ref Expression
jaoian (((𝜑𝜃) ∧ 𝜓) → 𝜒)

Proof of Theorem jaoian
StepHypRef Expression
1 jaoian.1 . . . 4 ((𝜑𝜓) → 𝜒)
21ex 416 . . 3 (𝜑 → (𝜓𝜒))
3 jaoian.2 . . . 4 ((𝜃𝜓) → 𝜒)
43ex 416 . . 3 (𝜃 → (𝜓𝜒))
52, 4jaoi 854 . 2 ((𝜑𝜃) → (𝜓𝜒))
65imp 410 1 (((𝜑𝜃) ∧ 𝜓) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 844 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845 This theorem is referenced by:  ccase  1033  preq12nebg  4753  opthprneg  4755  elpreqpr  4757  tpres  6941  xaddnemnf  12620  xaddnepnf  12621  faclbnd  13649  faclbnd3  13651  faclbnd4lem1  13652  znf1o  20248  degltlem1  24683  ipasslem3  28626  padct  30491  fz1nntr  30563  xrge0iifhom  31305  bj-ideqg1ALT  34599  fzsplit1nn0  39738
 Copyright terms: Public domain W3C validator