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

Theorem impl 649
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 452 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 448 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  sbc2iedv  3488  csbie2t  3543  frinxp  5145  ordelord  5704  foco2  6335  foco2OLD  6336  frxp  7232  mpt2curryd  7340  omsmolem  7678  erth  7736  unblem1  8156  unwdomg  8433  cflim2  9029  distrlem1pr  9791  uz11  11654  xmulge0  12057  max0add  13984  lcmfunsnlem2lem1  15275  divgcdcoprm0  15303  prmpwdvds  15532  imasleval  16122  dfgrp3lem  17434  resscntz  17685  ablfac1c  18391  lbsind  18999  mplcoe5lem  19386  cply1mul  19583  isphld  19918  smadiadetr  20400  chfacfisf  20578  chfacfisfcpmat  20579  chcoeffeq  20610  cayhamlem3  20611  tx1stc  21363  ioorcl  23251  coemullem  23910  xrlimcnp  24595  fsumdvdscom  24811  fsumvma  24838  cusgrres  26231  usgredgsscusgredg  26242  clwlkclwwlklem2a  26766  clwwlksext2edg  26789  frgr2wwlk1  27052  grpoidinvlem3  27209  htthlem  27623  atcvat4i  29105  abfmpeld  29296  isarchi3  29526  ordtconnlem1  29752  funpartfun  31692  relowlssretop  32843  ltflcei  33029  neificl  33181  keridl  33463  cvrat4  34209  ps-2  34244  mpaaeu  37201  clcnvlem  37411  iccpartiltu  40656  2pwp1prm  40802  bgoldbtbnd  40986  lmod0rng  41156  lincext1  41531
  Copyright terms: Public domain W3C validator