Theorem impl 458

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 418	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 420	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  sbc2iedv  3853  csbie2t  3923  frinxp  5636  ordelord  6215  foco2  6875  frxp  7822  mpocurryd  7937  omsmolem  8282  erth  8340  unblem1  8772  unwdomg  9050  cflim2  9687  distrlem1pr  10449  uz11  12270  elpq  12377  xmulge0  12680  max0add  14672  lcmfunsnlem2lem1  15984  divgcdcoprm0  16011  cncongr1  16013  prmpwdvds  16242  imasleval  16816  dfgrp3lem  18199  resscntz  18464  ablfac1c  19195  lbsind  19854  mplcoe5lem  20250  cply1mul  20464  isphld  20800  smadiadetr  21286  chfacfisf  21464  chfacfisfcpmat  21465  chcoeffeq  21496  cayhamlem3  21497  tx1stc  22260  ioorcl  24180  coemullem  24842  xrlimcnp  25548  fsumdvdscom  25764  fsumvma  25791  cusgrres  27232  usgredgsscusgredg  27243  clwlkclwwlklem2a  27778  clwwlkext2edg  27837  frgrwopreglem5ALT  28103  frgr2wwlkeu  28108  frgr2wwlk1  28110  grpoidinvlem3  28285  htthlem  28696  atcvat4i  30176  abfmpeld  30401  isarchi3  30818  qsidomlem2  30968  ordtconnlem1  31169  gonarlem  32643  fmlasucdisj  32648  funpartfun  33406  relowlssretop  34646  ltflcei  34882  neificl  35030  keridl  35312  eqvrelth  35848  cvrat4  36581  ps-2  36616  mpaaeu  39757  clcnvlem  39990  iccpartiltu  43589  2pwp1prm  43758  bgoldbtbnd  43981  lmod0rng  44146  lincext1  44516