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

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

Proof of Theorem imp32
StepHypRef Expression
1 imp31.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21impd 412 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
32imp 408 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  imp42  428  impr  456  anasss  468  an13s  650  3expb  1121  reuss2  4276  reupick  4279  po2nr  5560  tz7.7  6344  ordtr2  6362  fvmptt  6969  fliftfund  7259  isomin  7283  f1ocnv2d  7607  onint  7726  soseq  8092  tz7.48lem  8388  oalimcl  8508  oaass  8509  omass  8528  omabs  8598  finsschain  9304  frmin  9686  infxpenlem  9950  axcc3  10375  zorn2lem7  10439  addclpi  10829  addnidpi  10838  genpnnp  10942  genpnmax  10944  mulclprlem  10956  dedekindle  11320  prodgt0  12003  ltsubrp  12952  ltaddrp  12953  pfxccat3  14623  sumeven  16270  sumodd  16271  lcmfunsnlem2lem1  16515  divgcdcoprm0  16542  infpnlem1  16783  prmgaplem4  16927  iscatd  17554  imasmnd2  18594  imasgrp2  18863  cyccom  18997  imasring  20046  mplcoe5lem  21443  dmatmul  21849  scmatmulcl  21870  scmatsgrp1  21874  smatvscl  21876  cpmatacl  22068  cpmatmcllem  22070  0ntr  22425  clsndisj  22429  innei  22479  islpi  22503  tgcnp  22607  haust1  22706  alexsublem  23398  alexsubb  23400  isxmetd  23682  bddiblnc  25209  2lgslem1a1  26740  nodense  27043  axcontlem4  27919  ewlkle  28556  clwwlkf  28994  clwwlknonwwlknonb  29053  uhgr3cyclexlem  29128  numclwwlk1lem2foa  29301  grpoidinvlem3  29451  elspansn5  30519  5oalem6  30604  mdi  31240  dmdi  31247  dmdsl3  31260  atom1d  31298  cvexchlem  31313  atcvatlem  31330  chirredlem3  31337  mdsymlem5  31352  f1o3d  31544  bnj570  33520  dfon2lem6  34366  broutsideof2  34710  outsideoftr  34717  outsideofeq  34718  elicc3  34792  nn0prpwlem  34797  nndivsub  34932  fvineqsneu  35885  fvineqsneq  35886  ftc1anc  36162  cntotbnd  36258  heiborlem6  36278  pridlc3  36535  erimeq2  37143  leat2  37759  cvrexchlem  37885  cvratlem  37887  3dim2  37934  ps-2  37944  lncvrelatN  38247  osumcllem11N  38432  2reuimp0  45353  iccpartgt  45626  odz2prm2pw  45762  bgoldbachlt  46012  tgblthelfgott  46014  tgoldbach  46016  isomgrsym  46035  isomgrtr  46038  funcrngcsetcALT  46304
  Copyright terms: Public domain W3C validator