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

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

Proof of Theorem ad3antlr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21ad2antlr 480 . 2 (((𝜒𝜑) ∧ 𝜃) → 𝜓)
32adantr 274 1 ((((𝜒𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  ad4antlr  486  nntr2  6367  phpm  6727  phplem4on  6729  fidifsnen  6732  fisbth  6745  fin0  6747  fin0or  6748  fiintim  6785  fisseneq  6788  djudom  6946  difinfsnlem  6952  enomnilem  6978  prmuloc  7342  cauappcvgprlemopl  7422  cauappcvgprlemdisj  7427  cauappcvgprlemladdfl  7431  caucvgprlemopl  7445  axcaucvglemcau  7674  xaddf  9595  xleaddadd  9638  ssfzo12bi  9970  rebtwn2zlemstep  9998  btwnzge0  10041  addmodlteq  10139  frecuzrdgg  10157  hashxp  10540  cjap  10646  caucvgre  10721  minmax  10969  xrminmax  11002  sumeq2  11096  fsumconst  11191  bezoutlemmain  11613  dfgcd2  11629  lcmgcdlem  11685  cnpnei  12315  cnntr  12321  txmetcnp  12614  peano4nninf  13127  nninfalllemn  13129
  Copyright terms: Public domain W3C validator