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

Theorem adantll 453
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 107 . 2 ((𝜃𝜑) → 𝜑)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan 271 1 (((𝜃𝜑) ∧ 𝜓) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  ad2antlr  466  ad2ant2l  485  ad2ant2lr  487  3ad2antl3  1079  3adant1l  1138  reu6  2752  sbc2iegf  2855  sbcralt  2861  sbcrext  2862  indifdir  3220  pofun  4076  poinxp  4436  ssimaex  5261  fndmdif  5299  dffo4  5342  foco2  5345  fcompt  5360  fconst2g  5403  foeqcnvco  5457  f1eqcocnv  5458  fliftel1  5461  isores3  5482  acexmid  5538  tfrlemi14d  5977  dom2lem  6282  ordiso2  6414  lt2addnq  6559  lt2mulnq  6560  ltexnqq  6563  genpdf  6663  addnqprl  6684  addnqpru  6685  addlocpr  6691  recexprlemopl  6780  caucvgsrlemgt1  6936  add4  7234  cnegex  7251  ltleadd  7514  zextle  8388  peano5uzti  8404  fnn0ind  8412  xrlttr  8816  iccshftr  8962  iccshftl  8964  iccdil  8966  icccntr  8968  fzaddel  9023  fzrev  9047  expivallem  9415  expival  9416  mulexp  9453  expadd  9456  expmul  9459  leexp1a  9469  bccl  9628  ovshftex  9641  2shfti  9653  caucvgre  9801  cvg1nlemcau  9804  resqrexlemcvg  9838  cau3lem  9933  climmpt  10044  subcn2  10055  climrecvg1n  10090  climcvg1nlem  10091  climcaucn  10093  dvdsext  10159  sqoddm1div8z  10190  bj-findis  10463
  Copyright terms: Public domain W3C validator