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

Theorem adantll 445
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 103 . 2 ((𝜃𝜑) → 𝜑)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan 267 1 (((𝜃𝜑) ∧ 𝜓) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  ad2antlr  458  ad2ant2l  477  ad2ant2lr  479  3ad2antl3  1068  3adant1l  1127  reu6  2727  sbc2iegf  2825  sbcralt  2831  sbcrext  2832  indifdir  3190  pofun  4046  poinxp  4396  ssimaex  5221  fndmdif  5259  dffo4  5302  foco2  5305  fcompt  5320  fconst2g  5363  foeqcnvco  5417  f1eqcocnv  5418  fliftel1  5421  isores3  5442  acexmid  5498  tfrlemi14d  5934  dom2lem  6239  lt2addnq  6483  lt2mulnq  6484  ltexnqq  6487  genpdf  6587  addnqprl  6608  addnqpru  6609  addlocpr  6615  recexprlemopl  6704  caucvgsrlemgt1  6860  add4  7152  cnegex  7169  ltleadd  7419  zextle  8303  peano5uzti  8318  fnn0ind  8326  xrlttr  8683  iccshftr  8829  iccshftl  8831  iccdil  8833  icccntr  8835  fzaddel  8889  fzrev  8913  expivallem  9134  expival  9135  mulexp  9172  expadd  9175  expmul  9178  leexp1a  9187  ovshftex  9298  2shfti  9310  caucvgre  9458  cvg1nlemcau  9461  resqrexlemcvg  9495  cau3lem  9588  climmpt  9698  subcn2  9709  climrecvg1n  9744  climcvg1nlem  9745  climcaucn  9747  bj-findis  9977
  Copyright terms: Public domain W3C validator