Theorem 3adant3r3 1245

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 1235	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	2	3adantr3 1189	1 |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  imasmnd2  13818  imasmnd  13819  grpaddsubass  13954  grpsubsub4  13957  grpnpncan  13959  imasgrp2  13972  imasgrp  13973  cmn12  14199  abladdsub  14209  imasrng  14362  imasring  14478  opprrng  14491  opprring  14493  dvrass  14555  lss1  14808  mettri2  15588  xmetrtri  15602