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

Theorem jcab 903
 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 472 . . . 4 ((𝜓𝜒) → 𝜓)
21imim2i 16 . . 3 ((𝜑 → (𝜓𝜒)) → (𝜑𝜓))
3 simpr 476 . . . 4 ((𝜓𝜒) → 𝜒)
43imim2i 16 . . 3 ((𝜑 → (𝜓𝜒)) → (𝜑𝜒))
52, 4jca 553 . 2 ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) ∧ (𝜑𝜒)))
6 pm3.43 902 . 2 (((𝜑𝜓) ∧ (𝜑𝜒)) → (𝜑 → (𝜓𝜒)))
75, 6impbii 198 1 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ 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 196  df-an 385 This theorem is referenced by:  ordi  904  pm4.76  906  pm5.44  948  2mo2  2538  ssconb  3705  ssin  3797  tfr3  7382  trclfvcotr  13598  isprm2  15233  lgsquad2lem2  24910  ostthlem2  25117  pclclN  34195  ifpbibib  36874  elmapintrab  36901  elinintrab  36902  2reu4a  39838
 Copyright terms: Public domain W3C validator