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

Theorem adantll 467
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 109 . 2 ((𝜃𝜑) → 𝜑)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan 281 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:  ad2antlr  480  ad2ant2l  499  ad2ant2lr  501  3ad2antl3  1130  3adant1l  1193  reu6  2846  sbc2iegf  2951  sbcralt  2957  sbcrext  2958  indifdir  3302  pofun  4204  poinxp  4578  ssimaex  5450  fndmdif  5493  dffo4  5536  fcompt  5558  fconst2g  5603  foco2  5623  foeqcnvco  5659  f1eqcocnv  5660  fliftel1  5663  isores3  5684  acexmid  5741  tfrlemi14d  6198  tfrcl  6229  dom2lem  6634  fiintim  6785  ordiso2  6888  mkvprop  7000  lt2addnq  7180  lt2mulnq  7181  ltexnqq  7184  genpdf  7284  addnqprl  7305  addnqpru  7306  addlocpr  7312  recexprlemopl  7401  caucvgsrlemgt1  7571  add4  7891  cnegex  7908  ltleadd  8176  zextle  9100  peano5uzti  9117  fnn0ind  9125  xrlttr  9536  xaddass  9607  iccshftr  9732  iccshftl  9734  iccdil  9736  icccntr  9738  fzaddel  9794  fzrev  9819  exbtwnzlemshrink  9981  seq3val  10186  iseqf1olemab  10217  exp3vallem  10249  mulexp  10287  expadd  10290  expmul  10293  leexp1a  10303  bccl  10468  hashfacen  10534  ovshftex  10546  2shfti  10558  caucvgre  10708  cvg1nlemcau  10711  resqrexlemcvg  10746  cau3lem  10841  rexico  10948  iooinsup  11001  climmpt  11024  subcn2  11035  climrecvg1n  11072  climcvg1nlem  11073  climcaucn  11075  mertenslem2  11260  eftlcl  11308  reeftlcl  11309  dvdsext  11465  sqoddm1div8z  11495  bezoutlemaz  11603  bezoutr1  11633  dvdslcm  11662  lcmeq0  11664  lcmcl  11665  lcmneg  11667  lcmdvds  11672  coprmgcdb  11681  dvdsprime  11715  cnco  12301  cnss1  12306  tx2cn  12350  upxp  12352  metss  12574  txmetcnp  12598  cncfss  12650  cosz12  12772  bj-findis  13073
  Copyright terms: Public domain W3C validator