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  3797  csbie2t  3869  frinxp  5660  ordelord  6273  foco2  6965  frxp  7938  mpocurryd  8056  omsmolem  8447  erth  8505  unblem1  8996  unwdomg  9273  cflim2  9950  distrlem1pr  10712  uz11  12536  elpq  12644  xmulge0  12947  max0add  14950  lcmfunsnlem2lem1  16271  divgcdcoprm0  16298  cncongr1  16300  prmpwdvds  16533  imasleval  17169  dfgrp3lem  18588  resscntz  18853  ablfac1c  19589  lbsind  20257  isphld  20771  mplcoe5lem  21150  cply1mul  21375  smadiadetr  21732  chfacfisf  21911  chfacfisfcpmat  21912  chcoeffeq  21943  cayhamlem3  21944  tx1stc  22709  ioorcl  24646  coemullem  25316  xrlimcnp  26023  fsumdvdscom  26239  fsumvma  26266  cusgrres  27718  usgredgsscusgredg  27729  clwlkclwwlklem2a  28263  clwwlkext2edg  28321  frgrwopreglem5ALT  28587  frgr2wwlkeu  28592  frgr2wwlk1  28594  grpoidinvlem3  28769  htthlem  29180  atcvat4i  30660  abfmpeld  30893  ressupprn  30926  isarchi3  31343  qsidomlem2  31531  ordtconnlem1  31776  gonarlem  33256  fmlasucdisj  33261  funpartfun  34172  relowlssretop  35461  ltflcei  35692  neificl  35838  keridl  36117  eqvrelth  36651  cvrat4  37384  ps-2  37419  mpaaeu  40891  clcnvlem  41120  fcoresf1  44450  iccpartiltu  44762  2pwp1prm  44929  bgoldbtbnd  45149  lmod0rng  45314  lincext1  45683