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

Theorem jcab 925
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 924 . 2 (((𝜑𝜓) ∧ (𝜑𝜒)) → (𝜑 → (𝜓𝜒)))
75, 6impbii 199 1 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  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 197  df-an 385
This theorem is referenced by:  ordi  926  pm4.76  928  pm5.44  970  2mo2  2579  ssconb  3776  ssin  3868  tfr3  7540  trclfvcotr  13794  isprm2  15442  lgsquad2lem2  25155  ostthlem2  25362  pclclN  35495  ifpbibib  38172  elmapintrab  38199  elinintrab  38200  2reu4a  41510
  Copyright terms: Public domain W3C validator