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

Theorem 3ad2ant2 937
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 265 . 2 ((𝜑𝜃) → 𝜒)
323adant1 933 1 ((𝜓𝜑𝜃) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  simp2l  941  simp2r  942  simp21  948  simp22  949  simp23  950  simp2ll  982  simp2lr  983  simp2rl  984  simp2rr  985  simp2l1  1014  simp2l2  1015  simp2l3  1016  simp2r1  1017  simp2r2  1018  simp2r3  1019  simp21l  1032  simp21r  1033  simp22l  1034  simp22r  1035  simp23l  1036  simp23r  1037  simp211  1053  simp212  1054  simp213  1055  simp221  1056  simp222  1057  simp223  1058  simp231  1059  simp232  1060  simp233  1061  3anim123i  1100  3jaao  1214  ceqsalt  2597  vtoclgft  2621  vtoclegft  2642  ifbothdc  3384  frirrg  4114  elirr  4293  en2lp  4305  reg3exmidlemwe  4330  sotri3  4750  funtpg  4977  fnprg  4981  fntpg  4982  funimaexglem  5009  fnco  5034  fvun1  5266  oprssov  5669  caovimo  5721  rdgivallem  5998  f1dom2g  6266  ordiso2  6414  distrnqg  6542  distrnq0  6614  prarloclem5  6655  cauappcvgprlemlol  6802  cauappcvgprlemupu  6804  caucvgprlemlol  6825  caucvgprlemupu  6827  caucvgprprlemlol  6853  caucvgprprlemupu  6855  cnegexlem2  7249  apcotr  7671  apadd1  7672  mulext1  7676  div2negap  7785  ltdiv2  7927  nndivtr  8030  zdivmul  8387  gtndiv  8392  fzind  8411  eluzuzle  8576  eluzp1p1  8593  peano2uz  8621  qdivcl  8674  irrmul  8678  ledivge1le  8749  xrre2  8834  ubioc1  8898  ubicc2  8953  zltaddlt1le  8974  uzsubsubfz  9012  elfz1b  9053  fzp1nel  9067  fz0fzdiffz0  9088  difelfzle  9093  elfzo0  9139  elfzonlteqm1  9167  fzonn0p1p1  9170  fzosplitprm1  9191  fzoshftral  9195  subfzo0  9198  ceiqle  9257  modqval  9268  modqvalr  9269  flqpmodeq  9271  modq0  9273  mulqmod0  9274  negqmod0  9275  modqge0  9276  modqlt  9277  modqelico  9278  modqdiffl  9279  modqmulnn  9286  modqvalp1  9287  modqmuladdnn0  9312  qnegmod  9313  addmodid  9316  q2submod  9329  modifeq2int  9330  modfzo0difsn  9339  addmodlteq  9342  expival  9416  redivap  9695  imdivap  9702  climuni  10037  mulcn2  10056  summodnegmod  10130  pw2dvdslemn  10225
  Copyright terms: Public domain W3C validator