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

Theorem impl 447
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 404 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 408 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 198  df-an 385
This theorem is referenced by:  sbc2iedv  3665  csbie2t  3720  frinxp  5354  ordelord  5930  foco2  6569  frxp  7489  mpt2curryd  7598  omsmolem  7938  erth  7994  unblem1  8419  unwdomg  8696  cflim2  9338  distrlem1pr  10100  uz11  11909  xmulge0  12316  max0add  14337  lcmfunsnlem2lem1  15634  divgcdcoprm0  15661  cncongr1  15663  prmpwdvds  15889  imasleval  16469  dfgrp3lem  17782  resscntz  18029  ablfac1c  18737  lbsind  19352  mplcoe5lem  19741  cply1mul  19937  isphld  20274  smadiadetr  20759  chfacfisf  20938  chfacfisfcpmat  20939  chcoeffeq  20970  cayhamlem3  20971  tx1stc  21733  ioorcl  23635  coemullem  24297  xrlimcnp  24986  fsumdvdscom  25202  fsumvma  25229  cusgrres  26635  usgredgsscusgredg  26646  clwlkclwwlklem2a  27204  clwwlkext2edg  27269  frgrwopreglem5ALT  27560  frgr2wwlkeu  27565  frgr2wwlk1  27567  grpoidinvlem3  27752  htthlem  28165  atcvat4i  29647  abfmpeld  29839  isarchi3  30123  ordtconnlem1  30352  funpartfun  32426  relowlssretop  33576  ltflcei  33753  neificl  33903  keridl  34185  eqvrelth  34714  cvrat4  35331  ps-2  35366  mpaaeu  38329  clcnvlem  38537  iccpartiltu  42024  2pwp1prm  42111  bgoldbtbnd  42305  lmod0rng  42469  lincext1  42844
  Copyright terms: Public domain W3C validator