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  3866  csbie2t  3936  frinxp  5767  ordelord  6405  foco2  7128  f1ounsn  7293  frxp  8152  mpocurryd  8295  omsmolem  8696  erth  8797  unblem1  9329  unwdomg  9625  cflim2  10304  distrlem1pr  11066  uz11  12904  elpq  13018  xmulge0  13327  max0add  15350  lcmfunsnlem2lem1  16676  divgcdcoprm0  16703  cncongr1  16705  prmpwdvds  16943  imasleval  17587  issgrpd  18744  dfgrp3lem  19057  resscntz  19352  ablfac1c  20092  lbsind  21080  isphld  21673  mplcoe5lem  22058  cply1mul  22301  smadiadetr  22682  chfacfisf  22861  chfacfisfcpmat  22862  chcoeffeq  22893  cayhamlem3  22894  tx1stc  23659  ioorcl  25613  coemullem  26290  xrlimcnp  27012  fsumdvdscom  27229  fsumvma  27258  cusgrres  29467  usgredgsscusgredg  29478  clwlkclwwlklem2a  30018  clwwlkext2edg  30076  frgrwopreglem5ALT  30342  frgr2wwlkeu  30347  frgr2wwlk1  30349  grpoidinvlem3  30526  htthlem  30937  atcvat4i  32417  abfmpeld  32665  ressupprn  32700  isarchi3  33195  qsidomlem2  33482  ordtconnlem1  33924  gonarlem  35400  fmlasucdisj  35405  funpartfun  35945  relowlssretop  37365  ltflcei  37616  neificl  37761  keridl  38040  eqvrelth  38613  cvrat4  39446  ps-2  39481  mpaaeu  43167  clcnvlem  43641  fcoresf1  47086  iccpartiltu  47414  2pwp1prm  47581  bgoldbtbnd  47801  isuspgrimlem  47879  grimedg  47908  grimgrtri  47921  lmod0rng  48150  lincext1  48376