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

Theorem ad3antlr 485
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 481 . 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  487  nntr2  6406  phpm  6766  phplem4on  6768  fidifsnen  6771  fisbth  6784  fin0  6786  fin0or  6787  fiintim  6824  fisseneq  6827  djudom  6985  difinfsnlem  6991  enomnilem  7017  enmkvlem  7042  enwomnilem  7049  prmuloc  7397  cauappcvgprlemopl  7477  cauappcvgprlemdisj  7482  cauappcvgprlemladdfl  7486  caucvgprlemopl  7500  axcaucvglemcau  7729  xaddf  9656  xleaddadd  9699  ssfzo12bi  10032  rebtwn2zlemstep  10060  btwnzge0  10103  addmodlteq  10201  frecuzrdgg  10219  apexp1  10495  hashxp  10603  cjap  10709  caucvgre  10784  minmax  11032  xrminmax  11065  sumeq2  11159  fsumconst  11254  ntrivcvgap  11348  prodeq2  11357  bezoutlemmain  11720  dfgcd2  11736  lcmgcdlem  11792  cnpnei  12425  cnntr  12431  txmetcnp  12724  pw1nct  13369  peano4nninf  13373  nninfalllemn  13375
  Copyright terms: Public domain W3C validator