Theorem 3adant3r3 1238

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)

Hypothesis

Ref	Expression
3exp.1	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
3adant3r3	|- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )

Proof of Theorem 3adant3r3

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3expb 1228	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	2	3adantr3 1182	1 |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  imasmnd2  13485  imasmnd  13486  grpaddsubass  13623  grpsubsub4  13626  grpnpncan  13628  imasgrp2  13647  imasgrp  13648  cmn12  13843  abladdsub  13852  imasrng  13919  imasring  14027  opprrng  14040  opprring  14042  dvrass  14103  lss1  14326  mettri2  15036  xmetrtri  15050