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

Theorem 3ad2ant2 961
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 957 1 ((𝜓𝜑𝜃) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 920
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 922
This theorem is referenced by:  simp2l  965  simp2r  966  simp21  972  simp22  973  simp23  974  simp2ll  1006  simp2lr  1007  simp2rl  1008  simp2rr  1009  simp2l1  1038  simp2l2  1039  simp2l3  1040  simp2r1  1041  simp2r2  1042  simp2r3  1043  simp21l  1056  simp21r  1057  simp22l  1058  simp22r  1059  simp23l  1060  simp23r  1061  simp211  1077  simp212  1078  simp213  1079  simp221  1080  simp222  1081  simp223  1082  simp231  1083  simp232  1084  simp233  1085  3anim123i  1124  3jaao  1240  ceqsalt  2634  vtoclgft  2658  vtoclegft  2679  ifbothdc  3398  frirrg  4133  elirr  4312  en2lp  4325  reg3exmidlemwe  4349  sotri3  4773  funtpg  5001  fnprg  5005  fntpg  5006  funimaexglem  5033  fnco  5058  fvun1  5292  oprssov  5694  caovimo  5746  rdgivallem  6051  f1dom2g  6325  ssfidc  6477  ordiso2  6541  updjud  6576  distrnqg  6709  distrnq0  6781  prarloclem5  6822  cauappcvgprlemlol  6969  cauappcvgprlemupu  6971  caucvgprlemlol  6992  caucvgprlemupu  6994  caucvgprprlemlol  7020  caucvgprprlemupu  7022  cnegexlem2  7421  apcotr  7844  apadd1  7845  mulext1  7849  div2negap  7960  ltdiv2  8102  nndivtr  8217  zdivmul  8588  gtndiv  8593  fzind  8613  eluzuzle  8778  eluzp1p1  8795  peano2uz  8822  qdivcl  8879  irrmul  8883  ledivge1le  8954  xrre2  9034  ubioc1  9098  ubicc2  9153  zltaddlt1le  9174  uzsubsubfz  9212  elfz1b  9253  fzp1nel  9267  fz0fzdiffz0  9288  difelfzle  9292  elfzo0  9338  elfzonlteqm1  9366  fzonn0p1p1  9369  fzosplitprm1  9390  fzoshftral  9394  subfzo0  9398  ceiqle  9465  modqval  9476  modqvalr  9477  flqpmodeq  9479  modq0  9481  mulqmod0  9482  negqmod0  9483  modqge0  9484  modqlt  9485  modqelico  9486  modqdiffl  9487  modqmulnn  9494  modqvalp1  9495  modqmuladdnn0  9520  qnegmod  9521  addmodid  9524  q2submod  9537  modifeq2int  9538  modfzo0difsn  9547  addmodlteq  9550  expival  9645  omgadd  9896  hashun  9899  redivap  9980  imdivap  9987  climuni  10351  mulcn2  10370  summodnegmod  10452  divalglemex  10547  divalg  10549  modremain  10554  ndvdssub  10555  fldivndvdslt  10560  nndvdslegcd  10582  dfgcd2  10628  mulgcd  10630  mulgcdr  10632  gcddiv  10633  rplpwr  10641  rppwr  10642  qredeq  10703  divgcdcoprmex  10709  cncongr1  10710  cncongr2  10711  pw2dvdslemn  10768  hashgcdlem  10828  unennn  10835
  Copyright terms: Public domain W3C validator