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

Theorem adantll 476
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypothesis
Ref Expression
adant2.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
adantll (((𝜃𝜑) ∧ 𝜓) → 𝜒)

Proof of Theorem adantll
StepHypRef Expression
1 simpr 110 . 2 ((𝜃𝜑) → 𝜑)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan 283 1 (((𝜃𝜑) ∧ 𝜓) → 𝜒)
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:  ad2antlr  489  ad2ant2l  508  ad2ant2lr  510  ad5ant23  522  ad5ant24  523  ad5ant25  524  3ad2antl3  1161  3adant1l  1230  reu6  2926  sbc2iegf  3033  sbcralt  3039  sbcrext  3040  indifdir  3391  pofun  4308  poinxp  4691  ssimaex  5572  fndmdif  5616  dffo4  5659  fcompt  5681  fconst2g  5726  foco2  5748  foeqcnvco  5784  f1eqcocnv  5785  fliftel1  5788  isores3  5809  acexmid  5867  tfrlemi14d  6327  tfrcl  6358  dom2lem  6765  fiintim  6921  ordiso2  7027  mkvprop  7149  lt2addnq  7381  lt2mulnq  7382  ltexnqq  7385  genpdf  7485  addnqprl  7506  addnqpru  7507  addlocpr  7513  recexprlemopl  7602  caucvgsrlemgt1  7772  add4  8095  cnegex  8112  ltleadd  8380  zextle  9320  peano5uzti  9337  fnn0ind  9345  xrlttr  9769  xaddass  9843  iccshftr  9968  iccshftl  9970  iccdil  9972  icccntr  9974  fzaddel  10032  fzrev  10057  exbtwnzlemshrink  10222  seq3val  10431  iseqf1olemab  10462  exp3vallem  10494  mulexp  10532  expadd  10535  expmul  10538  leexp1a  10548  bccl  10718  hashfacen  10787  ovshftex  10799  2shfti  10811  caucvgre  10961  cvg1nlemcau  10964  resqrexlemcvg  10999  cau3lem  11094  rexico  11201  iooinsup  11256  climmpt  11279  subcn2  11290  climrecvg1n  11327  climcvg1nlem  11328  climcaucn  11330  mertenslem2  11515  eftlcl  11667  reeftlcl  11668  dvdsext  11831  sqoddm1div8z  11861  bezoutlemaz  11974  bezoutr1  12004  dvdslcm  12039  lcmeq0  12041  lcmcl  12042  lcmneg  12044  lcmdvds  12049  coprmgcdb  12058  dvdsprime  12092  pc2dvds  12299  prmpwdvds  12323  infpnlem1  12327  1arith  12335  mhmco  12751  mhmima  12752  dfgrp2  12779  mulgfng  12863  cnco  13354  cnss1  13359  tx2cn  13403  upxp  13405  metss  13627  txmetcnp  13651  cncfss  13703  cosz12  13834  bj-findis  14353
  Copyright terms: Public domain W3C validator