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  6579  tfrcllemaccex  6592  fimax2gtri  7159  en2eqpr  7167  unsnfidcex  7180  unsnfidcel  7181  fissfi  7216  ctssdc  7404  cauappcvgprlemloc  7967  caucvgprlemm  7983  caucvgprlemladdrl  7993  caucvgprlemlim  7996  caucvgprprlemml  8009  caucvgprprlemexbt  8021  caucvgprprlemlim  8026  suplocexprlemmu  8033  suplocexprlemloc  8036  suplocexprlemlub  8039  caucvgsrlemgt1  8110  suplocsrlemb  8121  suplocsrlem  8123  axcaucvglemres  8214  xaddval  10178  rebtwn2zlemstep  10612  nn0ltexp2  11071  hashunlem  11168  caucvgre  11666  cvg1nlemres  11670  resqrexlemglsq  11707  maxabslemval  11893  xrmaxiflemcl  11930  xrmaxifle  11931  xrmaxiflemab  11932  xrmaxiflemlub  11933  xrmaxiflemval  11935  xrmaxltsup  11943  divalglemeunn  12607  dvdsbnd  12652  bezoutlemnewy  12692  bezoutlemmain  12694  nninfctlemfo  12736  isprm5lem  12838  ctiunctlemfo  13190  prdsval  13486  sgrpidmndm  13633  mhmmnd  13833  mulgval  13839  txlm  15144  xmettx  15375  txmetcnp  15383  dedekindeu  15488  suplociccreex  15489  dedekindicclemlu  15495  dedekindicclemicc  15497  limcimo  15530  limccnp2cntop  15542  dvply2g  15631  lgsne0  15911  gfsumval  16862  gfsumz  16869