Theorem impl 461

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sbc2iedv  3819  csbie2t  3889  frinxp  5739  ordelord  6391  foco2  7120  f1ounsn  7290  frxp  8151  mpocurryd  8300  omsmolem  8680  erth  8786  unblem1  9298  unwdomg  9591  cflim2  10354  distrlem1pr  11123  uz11  13003  elpq  13116  xmulge0  13427  max0add  15492  lcmfunsnlem2lem1  16828  divgcdcoprm0  16855  cncongr1  16857  prmpwdvds  17097  imasleval  17728  issgrpd  18934  dfgrp3lem  19263  resscntz  19562  ablfac1c  20302  lbsind  21370  qsidomlem2  21652  isphld  21975  mplcoe5lem  22363  cply1mul  22629  smadiadetr  23005  chfacfisf  23187  chfacfisfcpmat  23188  chcoeffeq  23219  cayhamlem3  23220  tx1stc  23984  ioorcl  25913  coemullem  26584  xrlimcnp  27311  fsumdvdscom  27527  fsumvma  27555  cusgrres  30044  usgredgsscusgredg  30055  clwlkclwwlklem2a  30604  clwwlkext2edg  30662  frgrwopreglem5ALT  30938  frgr2wwlkeu  30943  frgr2wwlk1  30945  grpoidinvlem3  31123  htthlem  31534  atcvat4i  33014  abfmpeld  33305  ressupprn  33340  isarchi3  33804  ordtconnlem1  34612  soinfdom  35780  gonarlem  36283  fmlasucdisj  36288  funpartfun  36837  relowlssretop  38429  ltflcei  38674  neificl  38830  keridl  39109  eqvrelth  39770  cvrat4  40643  ps-2  40678  mpaaeu  44295  clcnvlem  44766  fcoresf1  48281  modlt0b  48581  iccpartiltu  48646  2pwp1prm  48816  bgoldbtbnd  49049  isuspgrimlem  49135  grimedg  49175  grimgrtri  49189  lmod0rng  49468  lincext1  49708