Theorem 3adantr3 1037

Description: Deduction adding a conjunct to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem 3adantr3

Step	Hyp	Ref	Expression
1		3adantr.1	. . . 4 |- ((ph /\ (ps /\ ch)) -> th)
2	1	ancoms 484	. . 3 |- (((ps /\ ch) /\ ph) -> th)
3	2	3adantl3 1034	. 2 |- (((ps /\ ch /\ ta) /\ ph) -> th)
4	3	ancoms 484	1 |- ((ph /\ (ps /\ ch /\ ta)) -> th)

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858

This theorem is referenced by:  3ad2antr1 1041  3ad2antr2 1042  3adant3r3 1079  dfwe2 3861  dfwe2OLD 3862  tgioolem 9192  lmle 9238  grpnpncan 9379  nvsubadd 9607  fipreima 10175  comptoppr 10332  dmdsl3 11887  dblsubvec 14817  conntoppr 15445  reconnlem1 15446  fipreimaOLD 15756  fzadd2 15791  mettrifi2 15848  iimulcl 15874  icoopnst 15876  iocopnst 15877  lincmb01icc 15879  sstotbnd 15936  totbndss 15937  pi1gp 16095  isdivrng2 16111  iscringd 16147  unichnidl 16179  osumcllem11 17374

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860

Copyright terms: Public domain