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

Theorem ad3antlr 484
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 480 . 2  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
32adantr 274 1  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )
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  9582  xleaddadd  9625  ssfzo12bi  9957  rebtwn2zlemstep  9985  btwnzge0  10028  addmodlteq  10126  frecuzrdgg  10144  hashxp  10527  cjap  10633  caucvgre  10708  minmax  10956  xrminmax  10989  sumeq2  11083  fsumconst  11178  bezoutlemmain  11598  dfgcd2  11614  lcmgcdlem  11670  cnpnei  12299  cnntr  12305  txmetcnp  12598  peano4nninf  13096  nninfalllemn  13098
  Copyright terms: Public domain W3C validator