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  3656  csbie2t  3711  frinxp  5324  ordelord  5888  foco2  6522  frxp  7438  mpt2curryd  7547  omsmolem  7887  erth  7943  unblem1  8368  unwdomg  8645  cflim2  9287  distrlem1pr  10049  uz11  11911  xmulge0  12319  max0add  14258  lcmfunsnlem2lem1  15559  divgcdcoprm0  15586  cncongr1  15588  prmpwdvds  15815  imasleval  16409  dfgrp3lem  17721  resscntz  17971  ablfac1c  18678  lbsind  19293  mplcoe5lem  19682  cply1mul  19879  isphld  20216  smadiadetr  20700  chfacfisf  20879  chfacfisfcpmat  20880  chcoeffeq  20911  cayhamlem3  20912  tx1stc  21674  ioorcl  23565  coemullem  24226  xrlimcnp  24916  fsumdvdscom  25132  fsumvma  25159  cusgrres  26579  usgredgsscusgredg  26590  clwlkclwwlklem2a  27148  clwwlkext2edg  27213  frgrwopreglem5ALT  27504  frgr2wwlkeu  27509  frgr2wwlk1  27511  grpoidinvlem3  27700  htthlem  28114  atcvat4i  29596  abfmpeld  29794  isarchi3  30081  ordtconnlem1  30310  funpartfun  32387  relowlssretop  33548  ltflcei  33730  neificl  33881  keridl  34163  cvrat4  35251  ps-2  35286  mpaaeu  38246  clcnvlem  38456  iccpartiltu  41886  2pwp1prm  42031  bgoldbtbnd  42225  lmod0rng  42396  lincext1  42771
  Copyright terms: Public domain W3C validator