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  6406  tfrcllemaccex  6419  fimax2gtri  6962  en2eqpr  6968  unsnfidcex  6981  unsnfidcel  6982  ctssdc  7179  cauappcvgprlemloc  7719  caucvgprlemm  7735  caucvgprlemladdrl  7745  caucvgprlemlim  7748  caucvgprprlemml  7761  caucvgprprlemexbt  7773  caucvgprprlemlim  7778  suplocexprlemmu  7785  suplocexprlemloc  7788  suplocexprlemlub  7791  caucvgsrlemgt1  7862  suplocsrlemb  7873  suplocsrlem  7875  axcaucvglemres  7966  xaddval  9920  rebtwn2zlemstep  10342  nn0ltexp2  10801  hashunlem  10896  caucvgre  11146  cvg1nlemres  11150  resqrexlemglsq  11187  maxabslemval  11373  xrmaxiflemcl  11410  xrmaxifle  11411  xrmaxiflemab  11412  xrmaxiflemlub  11413  xrmaxiflemval  11415  xrmaxltsup  11423  divalglemeunn  12086  dvdsbnd  12123  bezoutlemnewy  12163  bezoutlemmain  12165  nninfctlemfo  12207  isprm5lem  12309  ctiunctlemfo  12656  sgrpidmndm  13061  mhmmnd  13246  mulgval  13252  txlm  14515  xmettx  14746  txmetcnp  14754  dedekindeu  14859  suplociccreex  14860  dedekindicclemlu  14866  dedekindicclemicc  14868  limcimo  14901  limccnp2cntop  14913  dvply2g  15002  lgsne0  15279