Theorem ad4antr 494

Description: Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)

Hypothesis

Ref	Expression
ad2ant.1	|- ( ph -> ps )

Assertion

Ref	Expression
ad4antr	|- ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) -> ps )

Proof of Theorem ad4antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	ad3antrrr 492	. 2 |- ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) -> ps )
3	2	adantr 276	1 |- ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104

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 is referenced by:  ad5antr  496  tfr1onlemaccex  6457  tfrcllemaccex  6470  fimax2gtri  7024  en2eqpr  7030  unsnfidcex  7043  unsnfidcel  7044  ctssdc  7241  cauappcvgprlemloc  7800  caucvgprlemm  7816  caucvgprlemladdrl  7826  caucvgprlemlim  7829  caucvgprprlemml  7842  caucvgprprlemexbt  7854  caucvgprprlemlim  7859  suplocexprlemmu  7866  suplocexprlemloc  7869  suplocexprlemlub  7872  caucvgsrlemgt1  7943  suplocsrlemb  7954  suplocsrlem  7956  axcaucvglemres  8047  xaddval  10002  rebtwn2zlemstep  10432  nn0ltexp2  10891  hashunlem  10986  caucvgre  11407  cvg1nlemres  11411  resqrexlemglsq  11448  maxabslemval  11634  xrmaxiflemcl  11671  xrmaxifle  11672  xrmaxiflemab  11673  xrmaxiflemlub  11674  xrmaxiflemval  11676  xrmaxltsup  11684  divalglemeunn  12347  dvdsbnd  12392  bezoutlemnewy  12432  bezoutlemmain  12434  nninfctlemfo  12476  isprm5lem  12578  ctiunctlemfo  12925  prdsval  13220  sgrpidmndm  13367  mhmmnd  13567  mulgval  13573  txlm  14866  xmettx  15097  txmetcnp  15105  dedekindeu  15210  suplociccreex  15211  dedekindicclemlu  15217  dedekindicclemicc  15219  limcimo  15252  limccnp2cntop  15264  dvply2g  15353  lgsne0  15630