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

Theorem adantrr 463
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 107 . 2 ((𝜓𝜃) → 𝜓)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan2 280 1 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  ad2ant2r  493  ad2ant2lr  494  dn1dc  902  3ad2antr1  1104  xordidc  1331  po2nr  4066  sotricim  4080  fmptco  5356  fvtp1g  5395  dff13  5433  fcof1o  5454  isocnv  5476  isores2  5478  isoini  5482  f1oiso2  5491  acexmidlemab  5531  ovmpt2df  5657  offval  5744  xp1st  5817  1stconst  5867  cnvf1olem  5870  f1od2  5881  mpt2xopoveq  5883  nnaordi  6140  nnmordi  6148  erinxp  6239  dom2lem  6311  fundmen  6345  fidifsnen  6395  ltsonq  6639  lt2addnq  6645  lt2mulnq  6646  ltexnqq  6649  prarloclemarch2  6660  enq0sym  6673  genprndl  6762  genprndu  6763  prmuloc  6807  distrlem1prl  6823  distrlem1pru  6824  ltsopr  6837  ltexprlemdisj  6847  ltexprlemfl  6850  ltexprlemfu  6852  addcanprlemu  6856  ltaprg  6860  mulcmpblnrlemg  6968  recexgt0sr  7001  mul4  7296  2addsub  7378  muladd  7544  ltleadd  7606  divmulap3  7821  divcanap7  7865  divadddivap  7871  lemul2a  7993  lemul12b  7995  ltmuldiv2  8009  ltdivmul  8010  ltdivmul2  8012  ledivmul2  8014  lemuldiv2  8016  lt2msq  8020  cju  8094  zextlt  8509  xrlttr  8935  xrre3  8954  ixxdisj  8991  iooshf  9040  icodisj  9079  iccf1o  9091  expsubap  9610  ibcval5  9776  sqrt0rlem  10016  lenegsq  10108  ndvdsadd  10464  zssinfcl  10477  lcmdvds  10594  oddpwdclemdc  10684
  Copyright terms: Public domain W3C validator