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

Theorem 3ad2ant2 963
Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
Hypothesis
Ref Expression
3ad2ant.1 (𝜑𝜒)
Assertion
Ref Expression
3ad2ant2 ((𝜓𝜑𝜃) → 𝜒)

Proof of Theorem 3ad2ant2
StepHypRef Expression
1 3ad2ant.1 . . 3 (𝜑𝜒)
21adantr 270 . 2 ((𝜑𝜃) → 𝜒)
323adant1 959 1 ((𝜓𝜑𝜃) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 922
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 depends on definitions:  df-bi 115  df-3an 924
This theorem is referenced by:  simp2l  967  simp2r  968  simp21  974  simp22  975  simp23  976  simp2ll  1008  simp2lr  1009  simp2rl  1010  simp2rr  1011  simp2l1  1040  simp2l2  1041  simp2l3  1042  simp2r1  1043  simp2r2  1044  simp2r3  1045  simp21l  1058  simp21r  1059  simp22l  1060  simp22r  1061  simp23l  1062  simp23r  1063  simp211  1079  simp212  1080  simp213  1081  simp221  1082  simp222  1083  simp223  1084  simp231  1085  simp232  1086  simp233  1087  3anim123i  1126  3jaao  1242  ceqsalt  2639  vtoclgft  2663  vtoclegft  2684  ifbothdc  3409  frirrg  4151  elirr  4330  en2lp  4343  reg3exmidlemwe  4367  sotri3  4797  funtpg  5030  fnprg  5034  fntpg  5035  funimaexglem  5062  fnco  5087  fvun1  5333  oprssov  5743  caovimo  5795  rdgivallem  6100  f1dom2g  6425  mapxpen  6516  ssfidc  6594  sbthlemi4  6613  ordiso2  6672  updjud  6717  distrnqg  6890  distrnq0  6962  prarloclem5  7003  cauappcvgprlemlol  7150  cauappcvgprlemupu  7152  caucvgprlemlol  7173  caucvgprlemupu  7175  caucvgprprlemlol  7201  caucvgprprlemupu  7203  cnegexlem2  7602  apcotr  8025  apadd1  8026  mulext1  8030  div2negap  8141  ltdiv2  8283  nndivtr  8398  zdivmul  8769  gtndiv  8774  fzind  8794  eluzuzle  8959  eluzp1p1  8976  peano2uz  9003  qdivcl  9060  irrmul  9064  ledivge1le  9135  xrre2  9215  ubioc1  9279  ubicc2  9334  zltaddlt1le  9355  uzsubsubfz  9393  elfz1b  9434  fzp1nel  9448  fz0fzdiffz0  9469  difelfzle  9473  elfzo0  9521  elfzonlteqm1  9549  fzonn0p1p1  9552  fzosplitprm1  9573  fzoshftral  9577  subfzo0  9581  ceiqle  9648  modqval  9659  modqvalr  9660  flqpmodeq  9662  modq0  9664  mulqmod0  9665  negqmod0  9666  modqge0  9667  modqlt  9668  modqelico  9669  modqdiffl  9670  modqmulnn  9677  modqvalp1  9678  modqmuladdnn0  9703  qnegmod  9704  addmodid  9707  q2submod  9720  modifeq2int  9721  modfzo0difsn  9730  addmodlteq  9733  expival  9855  omgadd  10106  hashun  10109  redivap  10203  imdivap  10210  climuni  10574  mulcn2  10593  summodnegmod  10702  divalglemex  10797  divalg  10799  modremain  10804  ndvdssub  10805  fldivndvdslt  10810  nndvdslegcd  10832  dfgcd2  10878  mulgcd  10880  mulgcdr  10882  gcddiv  10883  rplpwr  10891  rppwr  10892  qredeq  10953  divgcdcoprmex  10959  cncongr1  10960  cncongr2  10961  pw2dvdslemn  11018  hashgcdlem  11078  unennn  11085
  Copyright terms: Public domain W3C validator