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

Theorem imp32 422
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 414 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
32imp 410 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  imp42  430  impr  458  anasss  470  an13s  650  3expb  1117  reuss2  4238  reupick  4242  po2nr  5455  tz7.7  6189  ordtr2  6207  fvmptt  6769  fliftfund  7049  isomin  7073  f1ocnv2d  7382  onint  7494  tz7.48lem  8064  oalimcl  8173  oaass  8174  omass  8193  omabs  8261  finsschain  8819  infxpenlem  9428  axcc3  9853  zorn2lem7  9917  addclpi  10307  addnidpi  10316  genpnnp  10420  genpnmax  10422  mulclprlem  10434  dedekindle  10797  prodgt0  11480  ltsubrp  12417  ltaddrp  12418  pfxccat3  14091  sumeven  15732  sumodd  15733  lcmfunsnlem2lem1  15976  divgcdcoprm0  16003  infpnlem1  16240  prmgaplem4  16384  iscatd  16940  imasmnd2  17944  imasgrp2  18210  cyccom  18342  imasring  19369  mplcoe5lem  20711  dmatmul  21106  scmatmulcl  21127  scmatsgrp1  21131  smatvscl  21133  cpmatacl  21325  cpmatmcllem  21327  0ntr  21680  clsndisj  21684  innei  21734  islpi  21758  tgcnp  21862  haust1  21961  alexsublem  22653  alexsubb  22655  isxmetd  22937  bddiblnc  24449  2lgslem1a1  25977  axcontlem4  26765  ewlkle  27399  clwwlkf  27836  clwwlknonwwlknonb  27895  uhgr3cyclexlem  27970  numclwwlk1lem2foa  28143  grpoidinvlem3  28293  elspansn5  29361  5oalem6  29446  mdi  30082  dmdi  30089  dmdsl3  30102  atom1d  30140  cvexchlem  30155  atcvatlem  30172  chirredlem3  30179  mdsymlem5  30194  f1o3d  30390  bnj570  32291  dfon2lem6  33147  frmin  33198  soseq  33210  nodense  33310  broutsideof2  33697  outsideoftr  33704  outsideofeq  33705  elicc3  33779  nn0prpwlem  33784  nndivsub  33919  fvineqsneu  34829  fvineqsneq  34830  ftc1anc  35137  cntotbnd  35233  heiborlem6  35253  pridlc3  35510  erim2  36070  leat2  36589  cvrexchlem  36714  cvratlem  36716  3dim2  36763  ps-2  36773  lncvrelatN  37076  osumcllem11N  37261  2reuimp0  43663  iccpartgt  43937  odz2prm2pw  44073  bgoldbachlt  44324  tgblthelfgott  44326  tgoldbach  44328  isomgrsym  44347  isomgrtr  44350  funcrngcsetcALT  44616
  Copyright terms: Public domain W3C validator