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  3805  csbie2t  3875  frinxp  5714  ordelord  6345  foco2  7061  f1ounsn  7227  frxp  8076  mpocurryd  8219  omsmolem  8593  erth  8698  unblem1  9202  unwdomg  9499  cflim2  10185  distrlem1pr  10948  uz11  12813  elpq  12925  xmulge0  13236  max0add  15272  lcmfunsnlem2lem1  16607  divgcdcoprm0  16634  cncongr1  16636  prmpwdvds  16875  imasleval  17505  issgrpd  18698  dfgrp3lem  19014  resscntz  19308  ablfac1c  20048  lbsind  21075  isphld  21634  mplcoe5lem  22017  cply1mul  22261  smadiadetr  22640  chfacfisf  22819  chfacfisfcpmat  22820  chcoeffeq  22851  cayhamlem3  22852  tx1stc  23615  ioorcl  25544  coemullem  26215  xrlimcnp  26932  fsumdvdscom  27148  fsumvma  27176  cusgrres  29517  usgredgsscusgredg  29528  clwlkclwwlklem2a  30068  clwwlkext2edg  30126  frgrwopreglem5ALT  30392  frgr2wwlkeu  30397  frgr2wwlk1  30399  grpoidinvlem3  30577  htthlem  30988  atcvat4i  32468  abfmpeld  32727  ressupprn  32763  isarchi3  33248  qsidomlem2  33513  ordtconnlem1  34068  gonarlem  35576  fmlasucdisj  35581  funpartfun  36125  relowlssretop  37679  ltflcei  37929  neificl  38074  keridl  38353  eqvrelth  39016  cvrat4  39889  ps-2  39924  mpaaeu  43578  clcnvlem  44050  fcoresf1  47517  modlt0b  47817  iccpartiltu  47882  2pwp1prm  48052  bgoldbtbnd  48285  isuspgrimlem  48371  grimedg  48411  grimgrtri  48425  lmod0rng  48705  lincext1  48930