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

Theorem impl 443
Description: Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.)
Hypothesis
Ref Expression
impl.1 (𝜑 → ((𝜓𝜒) → 𝜃))
Assertion
Ref Expression
impl (((𝜑𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem impl
StepHypRef Expression
1 impl.1 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
21expd 400 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 404 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 197  df-an 383
This theorem is referenced by:  sbc2iedv  3654  csbie2t  3709  frinxp  5324  ordelord  5888  foco2  6522  frxp  7437  mpt2curryd  7546  omsmolem  7886  erth  7942  unblem1  8367  unwdomg  8644  cflim2  9286  distrlem1pr  10048  uz11  11910  xmulge0  12318  max0add  14257  lcmfunsnlem2lem1  15558  divgcdcoprm0  15585  cncongr1  15587  prmpwdvds  15814  imasleval  16408  dfgrp3lem  17720  resscntz  17970  ablfac1c  18677  lbsind  19292  mplcoe5lem  19681  cply1mul  19878  isphld  20215  smadiadetr  20699  chfacfisf  20878  chfacfisfcpmat  20879  chcoeffeq  20910  cayhamlem3  20911  tx1stc  21673  ioorcl  23564  coemullem  24225  xrlimcnp  24915  fsumdvdscom  25131  fsumvma  25158  cusgrres  26578  usgredgsscusgredg  26589  clwlkclwwlklem2a  27145  clwwlkext2edg  27210  frgrwopreglem5ALT  27501  frgr2wwlkeu  27506  frgr2wwlk1  27508  grpoidinvlem3  27694  htthlem  28108  atcvat4i  29590  abfmpeld  29788  isarchi3  30075  ordtconnlem1  30304  funpartfun  32381  relowlssretop  33541  ltflcei  33723  neificl  33874  keridl  34156  cvrat4  35244  ps-2  35279  mpaaeu  38239  clcnvlem  38449  iccpartiltu  41876  2pwp1prm  42021  bgoldbtbnd  42215  lmod0rng  42386  lincext1  42761
  Copyright terms: Public domain W3C validator