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

Theorem 3ad2ant2 1004
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 274 . 2 ((𝜑𝜃) → 𝜒)
323adant1 1000 1 ((𝜓𝜑𝜃) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 965
This theorem is referenced by:  simp2l  1008  simp2r  1009  simp21  1015  simp22  1016  simp23  1017  simp2ll  1049  simp2lr  1050  simp2rl  1051  simp2rr  1052  simp2l1  1081  simp2l2  1082  simp2l3  1083  simp2r1  1084  simp2r2  1085  simp2r3  1086  simp21l  1099  simp21r  1100  simp22l  1101  simp22r  1102  simp23l  1103  simp23r  1104  simp211  1120  simp212  1121  simp213  1122  simp221  1123  simp222  1124  simp223  1125  simp231  1126  simp232  1127  simp233  1128  3anim123i  1167  3jaao  1287  ceqsalt  2713  vtoclgft  2737  vtoclegft  2759  ifbothdc  3505  frirrg  4276  elirr  4460  en2lp  4473  reg3exmidlemwe  4497  sotri3  4941  funtpg  5178  fnprg  5182  fntpg  5183  funimaexglem  5210  fnco  5235  fvun1  5491  oprssov  5916  caovimo  5968  rdgivallem  6282  fnsnsplitdc  6405  funresdfunsndc  6406  f1dom2g  6654  mapxpen  6746  ssfidc  6827  sbthlemi4  6852  ordiso2  6924  updjud  6971  difinfsn  6989  mkvprop  7036  endjudisj  7079  distrnqg  7215  distrnq0  7287  prarloclem5  7328  cauappcvgprlemlol  7475  cauappcvgprlemupu  7477  caucvgprlemlol  7498  caucvgprlemupu  7500  caucvgprprlemlol  7526  caucvgprprlemupu  7528  cnegexlem2  7958  apcotr  8389  apadd1  8390  mulext1  8394  div2negap  8515  ltdiv2  8665  nndivtr  8782  zdivmul  9161  gtndiv  9166  fzind  9186  eluzuzle  9354  eluzp1p1  9371  peano2uz  9401  qdivcl  9458  irrmul  9462  ledivge1le  9539  xrre2  9630  xaddass  9678  xltadd1  9685  xlt2add  9689  ubioc1  9738  ubicc2  9794  zltaddlt1le  9816  uzsubsubfz  9854  elfz1b  9897  fzp1nel  9911  fz0fzdiffz0  9934  difelfzle  9938  elfzo0  9986  elfzonlteqm1  10014  fzonn0p1p1  10017  fzosplitprm1  10038  fzoshftral  10042  subfzo0  10046  ceiqle  10113  modqval  10124  modqvalr  10125  flqpmodeq  10127  modq0  10129  mulqmod0  10130  negqmod0  10131  modqge0  10132  modqlt  10133  modqelico  10134  modqdiffl  10135  modqmulnn  10142  modqvalp1  10143  modqmuladdnn0  10168  qnegmod  10169  addmodid  10172  q2submod  10185  modifeq2int  10186  modfzo0difsn  10195  addmodlteq  10198  omgadd  10576  hashun  10579  redivap  10674  imdivap  10681  xrmaxltsup  11055  xrmaxadd  11058  xrlemininf  11068  xrminltinf  11069  climuni  11090  mulcn2  11109  fsumsplitsnun  11216  prodfap0  11342  efsub  11415  cos12dec  11501  summodnegmod  11551  divalglemex  11646  divalg  11648  modremain  11653  ndvdssub  11654  fldivndvdslt  11659  nndvdslegcd  11681  dfgcd2  11729  mulgcd  11731  mulgcdr  11733  gcddiv  11734  rplpwr  11742  rppwr  11743  qredeq  11804  divgcdcoprmex  11810  cncongr1  11811  cncongr2  11812  pw2dvdslemn  11870  hashgcdlem  11930  unennn  11937  ntrin  12323  elnei  12351  restco  12373  cnpnei  12418  cncnp2m  12430  sslm  12446  upxp  12471  blres  12633  metcnp3  12710  tgqioo  12746  ptolemy  12944  cxpcom  13056  logbgcd1irr  13083
  Copyright terms: Public domain W3C validator