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  6045  tfrcllemaccex  6058  en2eqpr  6550  unsnfidcex  6557  unsnfidcel  6558  cauappcvgprlemloc  7114  caucvgprlemm  7130  caucvgprlemladdrl  7140  caucvgprlemlim  7143  caucvgprprlemml  7156  caucvgprprlemexbt  7168  caucvgprprlemlim  7173  caucvgsrlemgt1  7243  axcaucvglemres  7337  rebtwn2zlemstep  9553  hashunlem  10047  caucvgre  10241  cvg1nlemres  10245  resqrexlemglsq  10282  maxabslemval  10468  sumeq2d  10570  divalglemeunn  10701  dvdsbnd  10728  bezoutlemnewy  10765  bezoutlemmain  10767
  Copyright terms: Public domain W3C validator