ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  adantrr Structured version   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  866  3ad2antr1  1068  xordidc  1287  po2nr  4037  sotricim  4051  fmptco  5273  fvtp1g  5312  dff13  5350  fcof1o  5372  isocnv  5394  isores2  5396  isoini  5400  f1oiso2  5409  acexmidlemab  5449  ovmpt2df  5574  offval  5661  xp1st  5734  1stconst  5784  cnvf1olem  5787  mpt2xopoveq  5796  nnaordi  6017  nnmordi  6025  erinxp  6116  dom2lem  6188  fundmen  6222  ltsonq  6382  lt2addnq  6388  ltexnqq  6391  prarloclemarch2  6402  enq0sym  6414  genprndl  6503  genprndu  6504  prmuloc  6546  distrlem1prl  6557  distrlem1pru  6558  ltsopr  6569  ltexprlemdisj  6579  ltexprlemfl  6582  ltexprlemfu  6584  addcanprlemu  6588  ltaprg  6591  mulcmpblnrlemg  6648  recexgt0sr  6681  mul4  6922  2addsub  7002  muladd  7157  ltleadd  7216  divmulap3  7418  divcanap7  7459  divadddivap  7465  lemul2a  7586  lemul12b  7588  ltmuldiv2  7602  ltdivmul  7603  ltdivmul2  7605  ledivmul2  7607  lemuldiv2  7609  lt2msq  7613  cju  7674  zextlt  8088  xrlttr  8466  xrre3  8485  ixxdisj  8522  iooshf  8571  icodisj  8610  iccf1o  8622  expsubap  8936  sqrt0rlem  9192
  Copyright terms: Public domain W3C validator