MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imp32 Structured version   Visualization version   GIF version

Theorem imp32 447
Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
impd.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
imp32 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)

Proof of Theorem imp32
StepHypRef Expression
1 impd.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21impd 445 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
32imp 443 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 195  df-an 384
This theorem is referenced by:  imp42  617  impr  646  anasss  676  an13s  840  3expb  1257  reuss2  3865  reupick  3869  po2nr  4962  tz7.7  5652  ordtr2  5671  fvmptt  6193  fliftfund  6441  isomin  6465  f1ocnv2d  6762  onint  6865  tz7.48lem  7401  oalimcl  7505  oaass  7506  omass  7525  omabs  7592  finsschain  8134  infxpenlem  8697  axcc3  9121  zorn2lem7  9185  addclpi  9571  addnidpi  9580  genpnnp  9684  genpnmax  9686  mulclprlem  9698  dedekindle  10053  prodgt0  10720  ltsubrp  11701  ltaddrp  11702  swrdccatin1  13283  swrdccat3  13292  sumeven  14897  sumodd  14898  lcmfunsnlem2lem1  15138  divgcdcoprm0  15166  infpnlem1  15401  prmgaplem4  15545  iscatd  16106  imasmnd2  17099  imasgrp2  17302  imasring  18391  mplcoe5lem  19237  dmatmul  20070  scmatmulcl  20091  scmatsgrp1  20095  smatvscl  20097  cpmatacl  20288  cpmatmcllem  20290  0ntr  20633  clsndisj  20637  innei  20687  islpi  20711  tgcnp  20815  haust1  20914  alexsublem  21606  alexsubb  21608  isxmetd  21889  2lgslem1a1  24859  axcontlem4  25593  wwlknimp  26009  wlkiswwlksur  26041  clwwlkf  26116  clwwlkextfrlem1  26397  grpoidinvlem3  26538  elspansn5  27651  5oalem6  27736  mdi  28372  dmdi  28379  dmdsl3  28392  atom1d  28430  cvexchlem  28445  atcvatlem  28462  chirredlem3  28469  mdsymlem5  28484  f1o3d  28647  bnj570  30063  dfon2lem6  30771  frmin  30817  soseq  30829  nodenselem5  30918  nodense  30922  broutsideof2  31233  outsideoftr  31240  outsideofeq  31241  elicc3  31315  nn0prpwlem  31321  nndivsub  31460  bddiblnc  32474  ftc1anc  32487  cntotbnd  32589  heiborlem6  32609  pridlc3  32866  leat2  33423  cvrexchlem  33547  cvratlem  33549  3dim2  33596  ps-2  33606  lncvrelatN  33909  osumcllem11N  34094  iccpartgt  39790  odz2prm2pw  39838  bgoldbachlt  40052  tgblthelfgott  40054  tgoldbach  40057  bgoldbachltOLD  40059  tgblthelfgottOLD  40061  tgoldbachOLD  40064  pfxccat3  40114  ewlkle  40829  wlkwwlksur  41116  clwwlksf  41244  uhgr3cyclexlem  41370  av-clwwlkextfrlem1  41531  funcrngcsetcALT  41813
  Copyright terms: Public domain W3C validator