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  2730  sbc2iegf  2828  sbcralt  2834  sbcrext  2835  indifdir  3193  pofun  4049  poinxp  4409  ssimaex  5234  fndmdif  5272  dffo4  5315  foco2  5318  fcompt  5333  fconst2g  5376  foeqcnvco  5430  f1eqcocnv  5431  fliftel1  5434  isores3  5455  acexmid  5511  tfrlemi14d  5947  dom2lem  6252  ordiso2  6357  lt2addnq  6502  lt2mulnq  6503  ltexnqq  6506  genpdf  6606  addnqprl  6627  addnqpru  6628  addlocpr  6634  recexprlemopl  6723  caucvgsrlemgt1  6879  add4  7172  cnegex  7189  ltleadd  7441  zextle  8331  peano5uzti  8346  fnn0ind  8354  xrlttr  8716  iccshftr  8862  iccshftl  8864  iccdil  8866  icccntr  8868  fzaddel  8922  fzrev  8946  expivallem  9256  expival  9257  mulexp  9294  expadd  9297  expmul  9300  leexp1a  9309  ovshftex  9420  2shfti  9432  caucvgre  9580  cvg1nlemcau  9583  resqrexlemcvg  9617  cau3lem  9710  climmpt  9821  subcn2  9832  climrecvg1n  9867  climcvg1nlem  9868  climcaucn  9870  bj-findis  10104
  Copyright terms: Public domain W3C validator