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

Theorem jaoian 859
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 197  df-or 384  df-an 385
This theorem is referenced by:  ccase  1024  elpreqpr  4503  tpres  6582  xaddnemnf  12181  xaddnepnf  12182  faclbnd  13192  faclbnd3  13194  faclbnd4lem1  13195  znf1o  20023  degltlem1  23952  ipasslem3  27918  padct  29727  fz1nntr  29791  xrge0iifhom  30213  fzsplit1nn0  37736
  Copyright terms: Public domain W3C validator