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  preq12nebg  4541  opthprneg  4543  elpreqpr  4545  tpres  6628  xaddnemnf  12258  xaddnepnf  12259  faclbnd  13269  faclbnd3  13271  faclbnd4lem1  13272  znf1o  20100  degltlem1  24029  ipasslem3  27995  padct  29804  fz1nntr  29868  xrge0iifhom  30290  fzsplit1nn0  37817
  Copyright terms: Public domain W3C validator