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

This theorem is referenced by:  sbc2iedv  3817  csbie2t  3887  frinxp  5707  ordelord  6339  foco2  7054  f1ounsn  7218  frxp  8068  mpocurryd  8211  omsmolem  8585  erth  8690  unblem1  9194  unwdomg  9491  cflim2  10175  distrlem1pr  10938  uz11  12778  elpq  12890  xmulge0  13201  max0add  15235  lcmfunsnlem2lem1  16567  divgcdcoprm0  16594  cncongr1  16596  prmpwdvds  16834  imasleval  17464  issgrpd  18657  dfgrp3lem  18970  resscntz  19264  ablfac1c  20004  lbsind  21034  isphld  21611  mplcoe5lem  21996  cply1mul  22242  smadiadetr  22621  chfacfisf  22800  chfacfisfcpmat  22801  chcoeffeq  22832  cayhamlem3  22833  tx1stc  23596  ioorcl  25536  coemullem  26213  xrlimcnp  26936  fsumdvdscom  27153  fsumvma  27182  cusgrres  29524  usgredgsscusgredg  29535  clwlkclwwlklem2a  30075  clwwlkext2edg  30133  frgrwopreglem5ALT  30399  frgr2wwlkeu  30404  frgr2wwlk1  30406  grpoidinvlem3  30583  htthlem  30994  atcvat4i  32474  abfmpeld  32734  ressupprn  32771  isarchi3  33271  qsidomlem2  33536  ordtconnlem1  34083  gonarlem  35590  fmlasucdisj  35595  funpartfun  36139  relowlssretop  37570  ltflcei  37811  neificl  37956  keridl  38235  eqvrelth  38890  cvrat4  39725  ps-2  39760  mpaaeu  43413  clcnvlem  43885  fcoresf1  47336  modlt0b  47630  iccpartiltu  47689  2pwp1prm  47856  bgoldbtbnd  48076  isuspgrimlem  48162  grimedg  48202  grimgrtri  48216  lmod0rng  48496  lincext1  48721