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  13817  imasmnd  13818  grpaddsubass  13953  grpsubsub4  13956  grpnpncan  13958  imasgrp2  13971  imasgrp  13972  cmn12  14198  abladdsub  14208  imasrng  14361  imasring  14477  opprrng  14490  opprring  14492  dvrass  14554  lss1  14807  mettri2  15605  xmetrtri  15619