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

Theorem jcab 517
Description: Distributive law for implication over conjunction. Compare Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 27-Nov-2013.)
Assertion
Ref Expression
jcab ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))

Proof of Theorem jcab
StepHypRef Expression
1 simpl 482 . . . 4 ((𝜓𝜒) → 𝜓)
21imim2i 16 . . 3 ((𝜑 → (𝜓𝜒)) → (𝜑𝜓))
3 simpr 484 . . . 4 ((𝜓𝜒) → 𝜒)
43imim2i 16 . . 3 ((𝜑 → (𝜓𝜒)) → (𝜑𝜒))
52, 4jca 511 . 2 ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) ∧ (𝜑𝜒)))
6 pm3.43 473 . 2 (((𝜑𝜓) ∧ (𝜑𝜒)) → (𝜑 → (𝜓𝜒)))
75, 6impbii 209 1 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395
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 207  df-an 396
This theorem is referenced by:  pm4.76  518  pm5.44  542  ordi  1008  2mo2  2647  ssconb  4142  ssin  4239  2reu4lem  4522  tfr3  8439  trclfvcotr  15048  isprm2  16719  lgsquad2lem2  27429  ostthlem2  27672  pclclN  39893  ifpbibib  43523  elmapintrab  43589  elinintrab  43590  ismnuprim  44313
  Copyright terms: Public domain W3C validator