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

Theorem jaoian 819
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 448 . . 3 (𝜑 → (𝜓𝜒))
3 jaoian.2 . . . 4 ((𝜃𝜓) → 𝜒)
43ex 448 . . 3 (𝜃 → (𝜓𝜒))
52, 4jaoi 392 . 2 ((𝜑𝜃) → (𝜓𝜒))
65imp 443 1 (((𝜑𝜃) ∧ 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 381  wa 382
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 195  df-or 383  df-an 384
This theorem is referenced by:  ccase  983  elpreqpr  4329  tpres  6348  xaddnemnf  11901  xaddnepnf  11902  faclbnd  12896  faclbnd3  12898  faclbnd4lem1  12899  znf1o  19666  degltlem1  23580  ipasslem3  26865  padct  28678  fz1nntr  28741  xrge0iifhom  29104  fzsplit1nn0  36118
  Copyright terms: Public domain W3C validator