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

Theorem ad4antr 478
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 476 . 2  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
32adantr 270 1  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  ad5antr  480  tfr1onlemaccex  6067  tfrcllemaccex  6080  fimax2gtri  6569  en2eqpr  6575  unsnfidcex  6582  unsnfidcel  6583  cauappcvgprlemloc  7155  caucvgprlemm  7171  caucvgprlemladdrl  7181  caucvgprlemlim  7184  caucvgprprlemml  7197  caucvgprprlemexbt  7209  caucvgprprlemlim  7214  caucvgsrlemgt1  7284  axcaucvglemres  7378  rebtwn2zlemstep  9592  hashunlem  10108  caucvgre  10309  cvg1nlemres  10313  resqrexlemglsq  10350  maxabslemval  10536  divalglemeunn  10796  dvdsbnd  10823  bezoutlemnewy  10860  bezoutlemmain  10862
  Copyright terms: Public domain W3C validator