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

Theorem jcab 861
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  |-  ( (
ph  ->  ( ps  /\  ch ) )  <->  ( ( ph  ->  ps )  /\  ( ph  ->  ch )
) )

Proof of Theorem jcab
StepHypRef Expression
1 simpl 455 . . . 4  |-  ( ( ps  /\  ch )  ->  ps )
21imim2i 14 . . 3  |-  ( (
ph  ->  ( ps  /\  ch ) )  ->  ( ph  ->  ps ) )
3 simpr 459 . . . 4  |-  ( ( ps  /\  ch )  ->  ch )
43imim2i 14 . . 3  |-  ( (
ph  ->  ( ps  /\  ch ) )  ->  ( ph  ->  ch ) )
52, 4jca 530 . 2  |-  ( (
ph  ->  ( ps  /\  ch ) )  ->  (
( ph  ->  ps )  /\  ( ph  ->  ch ) ) )
6 pm3.43 860 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ph  ->  ch ) )  ->  ( ph  ->  ( ps  /\  ch ) ) )
75, 6impbii 188 1  |-  ( (
ph  ->  ( ps  /\  ch ) )  <->  ( ( ph  ->  ps )  /\  ( ph  ->  ch )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367
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 185  df-an 369
This theorem is referenced by:  ordi  862  pm4.76  864  pm5.44  909  2mo2  2303  2eu4OLD  2312  ssconb  3551  ssin  3634  tfr3  6986  trclfvcotr  12847  isprm2  14227  lgsquad2lem2  23751  ostthlem2  23930  2reu4a  32360  pclclN  36028  ifpbibib  38143
  Copyright terms: Public domain W3C validator