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

Theorem ad4antr 478
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 476 . 2 ((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
32adantr 270 1 (((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
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  6069  tfrcllemaccex  6082  fimax2gtri  6571  en2eqpr  6577  unsnfidcex  6584  unsnfidcel  6585  cauappcvgprlemloc  7158  caucvgprlemm  7174  caucvgprlemladdrl  7184  caucvgprlemlim  7187  caucvgprprlemml  7200  caucvgprprlemexbt  7212  caucvgprprlemlim  7217  caucvgsrlemgt1  7287  axcaucvglemres  7381  rebtwn2zlemstep  9595  hashunlem  10112  caucvgre  10313  cvg1nlemres  10317  resqrexlemglsq  10354  maxabslemval  10540  divalglemeunn  10827  dvdsbnd  10854  bezoutlemnewy  10891  bezoutlemmain  10893
  Copyright terms: Public domain W3C validator