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

Theorem ad4antr 481
Description: Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad4antr (((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem ad4antr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21ad3antrrr 479 . 2 ((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
32adantr 272 1 (((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
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  483  tfr1onlemaccex  6175  tfrcllemaccex  6188  fimax2gtri  6724  en2eqpr  6730  unsnfidcex  6737  unsnfidcel  6738  ctssdc  6912  cauappcvgprlemloc  7361  caucvgprlemm  7377  caucvgprlemladdrl  7387  caucvgprlemlim  7390  caucvgprprlemml  7403  caucvgprprlemexbt  7415  caucvgprprlemlim  7420  caucvgsrlemgt1  7490  axcaucvglemres  7584  xaddval  9469  rebtwn2zlemstep  9871  hashunlem  10391  caucvgre  10593  cvg1nlemres  10597  resqrexlemglsq  10634  maxabslemval  10820  xrmaxiflemcl  10853  xrmaxifle  10854  xrmaxiflemab  10855  xrmaxiflemlub  10856  xrmaxiflemval  10858  xrmaxltsup  10866  divalglemeunn  11413  dvdsbnd  11440  bezoutlemnewy  11477  bezoutlemmain  11479  txlm  12229  limcimo  12514
  Copyright terms: Public domain W3C validator