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

Theorem ad4antr 483
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 481 . 2  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
32adantr 272 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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  ad5antr  485  tfr1onlemaccex  6199  tfrcllemaccex  6212  fimax2gtri  6748  en2eqpr  6754  unsnfidcex  6761  unsnfidcel  6762  ctssdc  6950  cauappcvgprlemloc  7408  caucvgprlemm  7424  caucvgprlemladdrl  7434  caucvgprlemlim  7437  caucvgprprlemml  7450  caucvgprprlemexbt  7462  caucvgprprlemlim  7467  caucvgsrlemgt1  7537  axcaucvglemres  7634  xaddval  9521  rebtwn2zlemstep  9923  hashunlem  10443  caucvgre  10645  cvg1nlemres  10649  resqrexlemglsq  10686  maxabslemval  10872  xrmaxiflemcl  10906  xrmaxifle  10907  xrmaxiflemab  10908  xrmaxiflemlub  10909  xrmaxiflemval  10911  xrmaxltsup  10919  divalglemeunn  11466  dvdsbnd  11493  bezoutlemnewy  11530  bezoutlemmain  11532  ctiunctlemfo  11795  txlm  12290  xmettx  12499  txmetcnp  12507  limcimo  12590  limccnp2cntop  12602
  Copyright terms: Public domain W3C validator