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

Theorem jaoian 820
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 449 . . 3 (𝜑 → (𝜓𝜒))
3 jaoian.2 . . . 4 ((𝜃𝜓) → 𝜒)
43ex 449 . . 3 (𝜃 → (𝜓𝜒))
52, 4jaoi 393 . 2 ((𝜑𝜃) → (𝜓𝜒))
65imp 444 1 (((𝜑𝜃) ∧ 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382  wa 383
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 196  df-or 384  df-an 385
This theorem is referenced by:  ccase  984  elpreqpr  4334  tpres  6371  xaddnemnf  11941  xaddnepnf  11942  faclbnd  12939  faclbnd3  12941  faclbnd4lem1  12942  znf1o  19719  degltlem1  23636  ipasslem3  27072  padct  28885  fz1nntr  28948  xrge0iifhom  29311  fzsplit1nn0  36335
  Copyright terms: Public domain W3C validator