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

Theorem adantrr 448
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
adantrr ((𝜑 ∧ (𝜓𝜃)) → 𝜒)

Proof of Theorem adantrr
StepHypRef Expression
1 simpl 102 . 2 ((𝜓𝜃) → 𝜓)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan2 270 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:  ad2ant2r  478  ad2ant2lr  479  dn1dc  867  3ad2antr1  1069  xordidc  1290  po2nr  4046  sotricim  4060  fmptco  5330  fvtp1g  5369  dff13  5407  fcof1o  5429  isocnv  5451  isores2  5453  isoini  5457  f1oiso2  5466  acexmidlemab  5506  ovmpt2df  5632  offval  5719  xp1st  5792  1stconst  5842  cnvf1olem  5845  mpt2xopoveq  5855  nnaordi  6081  nnmordi  6089  erinxp  6180  dom2lem  6252  fundmen  6286  fidifsnen  6331  ltsonq  6494  lt2addnq  6500  lt2mulnq  6501  ltexnqq  6504  prarloclemarch2  6515  enq0sym  6528  genprndl  6617  genprndu  6618  prmuloc  6662  distrlem1prl  6678  distrlem1pru  6679  ltsopr  6692  ltexprlemdisj  6702  ltexprlemfl  6705  ltexprlemfu  6707  addcanprlemu  6711  ltaprg  6715  mulcmpblnrlemg  6823  recexgt0sr  6856  mul4  7143  2addsub  7223  muladd  7379  ltleadd  7439  divmulap3  7654  divcanap7  7695  divadddivap  7701  lemul2a  7823  lemul12b  7825  ltmuldiv2  7839  ltdivmul  7840  ltdivmul2  7842  ledivmul2  7844  lemuldiv2  7846  lt2msq  7850  cju  7911  zextlt  8330  xrlttr  8714  xrre3  8733  ixxdisj  8770  iooshf  8819  icodisj  8858  iccf1o  8870  expsubap  9276  sqrt0rlem  9575  lenegsq  9665
  Copyright terms: Public domain W3C validator