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  6348  tfrcllemaccex  6361  fimax2gtri  6900  en2eqpr  6906  unsnfidcex  6918  unsnfidcel  6919  ctssdc  7111  cauappcvgprlemloc  7650  caucvgprlemm  7666  caucvgprlemladdrl  7676  caucvgprlemlim  7679  caucvgprprlemml  7692  caucvgprprlemexbt  7704  caucvgprprlemlim  7709  suplocexprlemmu  7716  suplocexprlemloc  7719  suplocexprlemlub  7722  caucvgsrlemgt1  7793  suplocsrlemb  7804  suplocsrlem  7806  axcaucvglemres  7897  xaddval  9844  rebtwn2zlemstep  10252  nn0ltexp2  10688  hashunlem  10783  caucvgre  10989  cvg1nlemres  10993  resqrexlemglsq  11030  maxabslemval  11216  xrmaxiflemcl  11252  xrmaxifle  11253  xrmaxiflemab  11254  xrmaxiflemlub  11255  xrmaxiflemval  11257  xrmaxltsup  11265  divalglemeunn  11925  dvdsbnd  11956  bezoutlemnewy  11996  bezoutlemmain  11998  isprm5lem  12140  ctiunctlemfo  12439  sgrpidmndm  12820  mhmmnd  12979  mulgval  12985  txlm  13749  xmettx  13980  txmetcnp  13988  dedekindeu  14071  suplociccreex  14072  dedekindicclemlu  14078  dedekindicclemicc  14080  limcimo  14104  limccnp2cntop  14116  lgsne0  14409