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  1007  2mo2  2645  ssconb  4152  ssin  4247  2reu4lem  4528  tfr3  8438  trclfvcotr  15045  isprm2  16716  lgsquad2lem2  27444  ostthlem2  27687  pclclN  39874  ifpbibib  43500  elmapintrab  43566  elinintrab  43567  ismnuprim  44290
  Copyright terms: Public domain W3C validator