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

Theorem ad3antlr 493
Description: Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
Hypothesis
Ref Expression
ad2ant.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ad3antlr  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )

Proof of Theorem ad3antlr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21ad2antlr 489 . 2  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
32adantr 276 1  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  ad4antlr  495  nntr2  6506  phpm  6867  phplem4on  6869  fidifsnen  6872  fisbth  6885  fin0  6887  fin0or  6888  fiintim  6930  fisseneq  6933  djudom  7094  difinfsnlem  7100  nnnninfeq  7128  nnnninfeq2  7129  enomnilem  7138  enmkvlem  7161  enwomnilem  7169  exmidapne  7261  prmuloc  7567  cauappcvgprlemopl  7647  cauappcvgprlemdisj  7652  cauappcvgprlemladdfl  7656  caucvgprlemopl  7670  axcaucvglemcau  7899  xnn0letri  9805  xaddf  9846  xleaddadd  9889  ssfzo12bi  10227  rebtwn2zlemstep  10255  btwnzge0  10302  addmodlteq  10400  frecuzrdgg  10418  qsqeqor  10633  apexp1  10700  hashxp  10808  cjap  10917  caucvgre  10992  minmax  11240  xrminmax  11275  sumeq2  11369  fsumconst  11464  ntrivcvgap  11558  prodeq2  11567  p1modz1  11803  bezoutlemmain  12001  dfgcd2  12017  uzwodc  12040  lcmgcdlem  12079  mulgval  12991  cnpnei  13758  cnntr  13764  txmetcnp  14057  lgsval  14444  pw1nct  14791  peano4nninf  14794
  Copyright terms: Public domain W3C validator