ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ad4antr Unicode version

Theorem ad4antr 486
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
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21ad3antrrr 484 . 2  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
32adantr 274 1  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  ad5antr  488  tfr1onlemaccex  6252  tfrcllemaccex  6265  fimax2gtri  6802  en2eqpr  6808  unsnfidcex  6815  unsnfidcel  6816  ctssdc  7005  cauappcvgprlemloc  7483  caucvgprlemm  7499  caucvgprlemladdrl  7509  caucvgprlemlim  7512  caucvgprprlemml  7525  caucvgprprlemexbt  7537  caucvgprprlemlim  7542  suplocexprlemmu  7549  suplocexprlemloc  7552  suplocexprlemlub  7555  caucvgsrlemgt1  7626  suplocsrlemb  7637  suplocsrlem  7639  axcaucvglemres  7730  xaddval  9657  rebtwn2zlemstep  10060  hashunlem  10581  caucvgre  10784  cvg1nlemres  10788  resqrexlemglsq  10825  maxabslemval  11011  xrmaxiflemcl  11045  xrmaxifle  11046  xrmaxiflemab  11047  xrmaxiflemlub  11048  xrmaxiflemval  11050  xrmaxltsup  11058  divalglemeunn  11652  dvdsbnd  11679  bezoutlemnewy  11718  bezoutlemmain  11720  ctiunctlemfo  11986  txlm  12485  xmettx  12716  txmetcnp  12724  dedekindeu  12807  suplociccreex  12808  dedekindicclemlu  12814  dedekindicclemicc  12816  limcimo  12840  limccnp2cntop  12852
  Copyright terms: Public domain W3C validator