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  3813  csbie2t  3883  frinxp  5697  ordelord  6328  foco2  7042  f1ounsn  7206  frxp  8056  mpocurryd  8199  omsmolem  8572  erth  8676  unblem1  9176  unwdomg  9470  cflim2  10154  distrlem1pr  10916  uz11  12757  elpq  12873  xmulge0  13183  max0add  15217  lcmfunsnlem2lem1  16549  divgcdcoprm0  16576  cncongr1  16578  prmpwdvds  16816  imasleval  17445  issgrpd  18638  dfgrp3lem  18951  resscntz  19245  ablfac1c  19985  lbsind  21014  isphld  21591  mplcoe5lem  21974  cply1mul  22211  smadiadetr  22590  chfacfisf  22769  chfacfisfcpmat  22770  chcoeffeq  22801  cayhamlem3  22802  tx1stc  23565  ioorcl  25505  coemullem  26182  xrlimcnp  26905  fsumdvdscom  27122  fsumvma  27151  cusgrres  29427  usgredgsscusgredg  29438  clwlkclwwlklem2a  29978  clwwlkext2edg  30036  frgrwopreglem5ALT  30302  frgr2wwlkeu  30307  frgr2wwlk1  30309  grpoidinvlem3  30486  htthlem  30897  atcvat4i  32377  abfmpeld  32636  ressupprn  32671  isarchi3  33156  qsidomlem2  33418  ordtconnlem1  33937  gonarlem  35438  fmlasucdisj  35443  funpartfun  35987  relowlssretop  37407  ltflcei  37658  neificl  37803  keridl  38082  eqvrelth  38717  cvrat4  39552  ps-2  39587  mpaaeu  43253  clcnvlem  43726  fcoresf1  47179  modlt0b  47473  iccpartiltu  47532  2pwp1prm  47699  bgoldbtbnd  47919  isuspgrimlem  48005  grimedg  48045  grimgrtri  48059  lmod0rng  48339  lincext1  48565