Theorem impl 456

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  sbc2iedv  3858  csbie2t  3930  frinxp  5750  ordelord  6375  foco2  7093  frxp  8094  mpocurryd  8236  omsmolem  8639  erth  8735  unblem1  9278  unwdomg  9561  cflim2  10240  distrlem1pr  11002  uz11  12829  elpq  12941  xmulge0  13245  max0add  15239  lcmfunsnlem2lem1  16557  divgcdcoprm0  16584  cncongr1  16586  prmpwdvds  16819  imasleval  17469  dfgrp3lem  18895  resscntz  19162  ablfac1c  19900  lbsind  20640  isphld  21140  mplcoe5lem  21522  cply1mul  21747  smadiadetr  22106  chfacfisf  22285  chfacfisfcpmat  22286  chcoeffeq  22317  cayhamlem3  22318  tx1stc  23083  ioorcl  25023  coemullem  25693  xrlimcnp  26400  fsumdvdscom  26616  fsumvma  26643  cusgrres  28570  usgredgsscusgredg  28581  clwlkclwwlklem2a  29116  clwwlkext2edg  29174  frgrwopreglem5ALT  29440  frgr2wwlkeu  29445  frgr2wwlk1  29447  grpoidinvlem3  29622  htthlem  30033  atcvat4i  31513  abfmpeld  31748  ressupprn  31783  isarchi3  32204  qsidomlem2  32423  ordtconnlem1  32735  gonarlem  34216  fmlasucdisj  34221  funpartfun  34745  relowlssretop  36048  ltflcei  36280  neificl  36426  keridl  36705  eqvrelth  37286  cvrat4  38119  ps-2  38154  mpaaeu  41663  clcnvlem  42145  fcoresf1  45551  iccpartiltu  45862  2pwp1prm  46029  bgoldbtbnd  46249  lmod0rng  46414  lincext1  46783