Theorem 3anim123d 1406

Description: Deduction joining 3 implications to form implication of conjunctions. (Contributed by NM, 24-Feb-2005.)

Hypotheses

Ref	Expression
3anim123d.1	|- ( ph -> ( ps -> ch ) )
3anim123d.2	|- ( ph -> ( th -> ta ) )
3anim123d.3	|- ( ph -> ( et -> ze ) )

Assertion

Ref	Expression
3anim123d	|- ( ph -> ( ( ps /\ th /\ et ) -> ( ch /\ ta /\ ze ) ) )

Proof of Theorem 3anim123d

Step	Hyp	Ref	Expression
1		3anim123d.1	. . . 4 |- ( ph -> ( ps -> ch ) )
2		3anim123d.2	. . . 4 |- ( ph -> ( th -> ta ) )
3	1, 2	anim12d 586	. . 3 |- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )
4		3anim123d.3	. . 3 |- ( ph -> ( et -> ze ) )
5	3, 4	anim12d 586	. 2 |- ( ph -> ( ( ( ps /\ th ) /\ et ) -> ( ( ch /\ ta ) /\ ze ) ) )
6		df-3an 1039	. 2 |- ( ( ps /\ th /\ et ) <-> ( ( ps /\ th ) /\ et ) )
7		df-3an 1039	. 2 |- ( ( ch /\ ta /\ ze ) <-> ( ( ch /\ ta ) /\ ze ) )
8	5, 6, 7	3imtr4g 285	1 |- ( ph -> ( ( ps /\ th /\ et ) -> ( ch /\ ta /\ ze ) ) )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 386  df-3an 1039

This theorem is referenced by:  pofun  5051  isopolem  6595  issmo2  7446  smores  7449  inawina  9512  gchina  9521  repswcshw  13558  coprmprod  15375  issubmnd  17318  issubg2  17609  issubrg2  18800  ocv2ss  20017  sslm  21103  cmetcaulem  23086  axcontlem4  25847  axcontlem8  25851  redwlk  26569  clwwlksnwwlksn  27209  numclwlk1lem2foa  27224  dipsubdir  27703  cgr3tr4  32159  idinside  32191  ftc1anclem7  33491  fzmul  33537  fdc1  33542  rngosubdi  33744  rngosubdir  33745  cdlemg33a  35994  upwlkwlk  41720  lidlmsgrp  41926  lidlrng  41927