Theorem impl 455

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

Step	Hyp	Ref	Expression
1		impl.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 415	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 417	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  sbc2iedv  3819  csbie2t  3889  frinxp  5702  ordelord  6329  foco2  7043  f1ounsn  7209  frxp  8059  mpocurryd  8202  omsmolem  8575  erth  8679  unblem1  9181  unwdomg  9476  cflim2  10157  distrlem1pr  10919  uz11  12760  elpq  12876  xmulge0  13186  max0add  15217  lcmfunsnlem2lem1  16549  divgcdcoprm0  16576  cncongr1  16578  prmpwdvds  16816  imasleval  17445  issgrpd  18604  dfgrp3lem  18917  resscntz  19212  ablfac1c  19952  lbsind  20984  isphld  21561  mplcoe5lem  21944  cply1mul  22181  smadiadetr  22560  chfacfisf  22739  chfacfisfcpmat  22740  chcoeffeq  22771  cayhamlem3  22772  tx1stc  23535  ioorcl  25476  coemullem  26153  xrlimcnp  26876  fsumdvdscom  27093  fsumvma  27122  cusgrres  29394  usgredgsscusgredg  29405  clwlkclwwlklem2a  29942  clwwlkext2edg  30000  frgrwopreglem5ALT  30266  frgr2wwlkeu  30271  frgr2wwlk1  30273  grpoidinvlem3  30450  htthlem  30861  atcvat4i  32341  abfmpeld  32598  ressupprn  32633  isarchi3  33130  qsidomlem2  33391  ordtconnlem1  33897  gonarlem  35377  fmlasucdisj  35382  funpartfun  35927  relowlssretop  37347  ltflcei  37598  neificl  37743  keridl  38022  eqvrelth  38598  cvrat4  39432  ps-2  39467  mpaaeu  43133  clcnvlem  43606  fcoresf1  47063  modlt0b  47357  iccpartiltu  47416  2pwp1prm  47583  bgoldbtbnd  47803  isuspgrimlem  47889  grimedg  47929  grimgrtri  47943  lmod0rng  48223  lincext1  48449