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

Theorem jcab 518
 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 483 . . . 4 ((𝜓𝜒) → 𝜓)
21imim2i 16 . . 3 ((𝜑 → (𝜓𝜒)) → (𝜑𝜓))
3 simpr 485 . . . 4 ((𝜓𝜒) → 𝜒)
43imim2i 16 . . 3 ((𝜑 → (𝜓𝜒)) → (𝜑𝜒))
52, 4jca 512 . 2 ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) ∧ (𝜑𝜒)))
6 pm3.43 474 . 2 (((𝜑𝜓) ∧ (𝜑𝜒)) → (𝜑 → (𝜓𝜒)))
75, 6impbii 210 1 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396 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 208  df-an 397 This theorem is referenced by:  pm4.76  519  pm5.44  543  ordi  1001  2mo2  2731  ssconb  4118  ssin  4211  2reu4lem  4468  tfr3  8031  trclfvcotr  14364  isprm2  16021  lgsquad2lem2  25894  ostthlem2  26137  pclclN  36913  ifpbibib  39760  elmapintrab  39820  elinintrab  39821  ismnuprim  40514
 Copyright terms: Public domain W3C validator