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

Theorem impl 648
 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 451 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 447 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  sbc2iedv  3473  csbie2t  3528  frinxp  5107  ordelord  5662  foco2  6287  foco2OLD  6288  frxp  7174  mpt2curryd  7282  omsmolem  7620  erth  7678  unblem1  8097  unwdomg  8372  cflim2  8968  distrlem1pr  9726  uz11  11586  xmulge0  11986  max0add  13898  lcmfunsnlem2lem1  15189  divgcdcoprm0  15217  prmpwdvds  15446  imasleval  16024  dfgrp3lem  17336  resscntz  17587  ablfac1c  18293  lbsind  18901  mplcoe5lem  19288  cply1mul  19485  isphld  19818  smadiadetr  20300  chfacfisf  20478  chfacfisfcpmat  20479  chcoeffeq  20510  cayhamlem3  20511  tx1stc  21263  ioorcl  23151  coemullem  23810  xrlimcnp  24495  fsumdvdscom  24711  fsumvma  24738  clwlkisclwwlklem2a  26313  clwwlkext2edg  26330  frg2wot1  26584  grpoidinvlem3  26744  htthlem  27158  atcvat4i  28640  abfmpeld  28834  isarchi3  29072  ordtconlem1  29298  funpartfun  31220  relowlssretop  32387  ltflcei  32567  neificl  32719  keridl  33001  cvrat4  33747  ps-2  33782  mpaaeu  36739  clcnvlem  36949  iccpartiltu  39960  2pwp1prm  40041  bgoldbtbnd  40225  cusgrres  40664  usgredgsscusgredg  40675  clwlkclwwlklem2a  41207  clwwlksext2edg  41230  frgr2wwlk1  41494  lmod0rng  41658  lincext1  42037
 Copyright terms: Public domain W3C validator