Theorem 3adant3r1 1243

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

Hypothesis

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

Assertion

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

Proof of Theorem 3adant3r1

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3expb 1235	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	2	3adantr1 1187	1 |- ( ( ph /\ ( ta /\ ps /\ ch ) ) -> 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:  ccatswrd  11442  imasmnd2  13759  grpsubsub  13894  grpnnncan2  13902  imasgrp2  13913  mulgnn0ass  13961  mulgsubdir  13965  cmn32  14107  ablsubadd  14116  imasrng  14255  imasring  14369  opprrng  14382  opprring  14384  xmettri3  15475  mettri3  15476  xmetrtri  15477  rprelogbmulexp  16058