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

This theorem is referenced by:  sbc2iedv  3858  csbie2t  3930  frinxp  5754  ordelord  6385  foco2  7113  frxp  8125  mpocurryd  8268  omsmolem  8671  erth  8768  unblem1  9311  unwdomg  9599  cflim2  10278  distrlem1pr  11040  uz11  12869  elpq  12981  xmulge0  13287  max0add  15281  lcmfunsnlem2lem1  16600  divgcdcoprm0  16627  cncongr1  16629  prmpwdvds  16864  imasleval  17514  issgrpd  18681  dfgrp3lem  18985  resscntz  19275  ablfac1c  20019  lbsind  20954  isphld  21573  mplcoe5lem  21964  cply1mul  22202  smadiadetr  22564  chfacfisf  22743  chfacfisfcpmat  22744  chcoeffeq  22775  cayhamlem3  22776  tx1stc  23541  ioorcl  25493  coemullem  26171  xrlimcnp  26887  fsumdvdscom  27104  fsumvma  27133  cusgrres  29249  usgredgsscusgredg  29260  clwlkclwwlklem2a  29795  clwwlkext2edg  29853  frgrwopreglem5ALT  30119  frgr2wwlkeu  30124  frgr2wwlk1  30126  grpoidinvlem3  30303  htthlem  30714  atcvat4i  32194  abfmpeld  32423  ressupprn  32454  isarchi3  32873  qsidomlem2  33105  ordtconnlem1  33461  gonarlem  34940  fmlasucdisj  34945  funpartfun  35475  relowlssretop  36778  ltflcei  37016  neificl  37161  keridl  37440  eqvrelth  38020  cvrat4  38853  ps-2  38888  mpaaeu  42496  clcnvlem  42976  fcoresf1  46374  iccpartiltu  46685  2pwp1prm  46852  bgoldbtbnd  47072  isuspgrimlem  47095  lmod0rng  47214  lincext1  47445