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

Theorem adantll 468
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  481  ad2ant2l  500  ad2ant2lr  502  ad5ant23  514  ad5ant24  515  ad5ant25  516  3ad2antl3  1146  3adant1l  1209  reu6  2876  sbc2iegf  2982  sbcralt  2988  sbcrext  2989  indifdir  3336  pofun  4241  poinxp  4615  ssimaex  5489  fndmdif  5532  dffo4  5575  fcompt  5597  fconst2g  5642  foco2  5662  foeqcnvco  5698  f1eqcocnv  5699  fliftel1  5702  isores3  5723  acexmid  5780  tfrlemi14d  6237  tfrcl  6268  dom2lem  6673  fiintim  6824  ordiso2  6927  mkvprop  7039  lt2addnq  7235  lt2mulnq  7236  ltexnqq  7239  genpdf  7339  addnqprl  7360  addnqpru  7361  addlocpr  7367  recexprlemopl  7456  caucvgsrlemgt1  7626  add4  7946  cnegex  7963  ltleadd  8231  zextle  9165  peano5uzti  9182  fnn0ind  9190  xrlttr  9610  xaddass  9681  iccshftr  9806  iccshftl  9808  iccdil  9810  icccntr  9812  fzaddel  9869  fzrev  9894  exbtwnzlemshrink  10056  seq3val  10261  iseqf1olemab  10292  exp3vallem  10324  mulexp  10362  expadd  10365  expmul  10368  leexp1a  10378  bccl  10544  hashfacen  10610  ovshftex  10622  2shfti  10634  caucvgre  10784  cvg1nlemcau  10787  resqrexlemcvg  10822  cau3lem  10917  rexico  11024  iooinsup  11077  climmpt  11100  subcn2  11111  climrecvg1n  11148  climcvg1nlem  11149  climcaucn  11151  mertenslem2  11336  eftlcl  11429  reeftlcl  11430  dvdsext  11587  sqoddm1div8z  11617  bezoutlemaz  11725  bezoutr1  11755  dvdslcm  11784  lcmeq0  11786  lcmcl  11787  lcmneg  11789  lcmdvds  11794  coprmgcdb  11803  dvdsprime  11837  cnco  12427  cnss1  12432  tx2cn  12476  upxp  12478  metss  12700  txmetcnp  12724  cncfss  12776  cosz12  12907  bj-findis  13346
  Copyright terms: Public domain W3C validator