Theorem impl 456

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 416	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 418	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  sbc2iedv  3799  csbie2t  3869  frinxp  5702  ordelord  6333  foco2  7051  f1ounsn  7217  frxp  8067  mpocurryd  8210  omsmolem  8584  erth  8689  unblem1  9193  unwdomg  9490  cflim2  10177  distrlem1pr  10940  uz11  12805  elpq  12917  xmulge0  13228  max0add  15264  lcmfunsnlem2lem1  16599  divgcdcoprm0  16626  cncongr1  16628  prmpwdvds  16867  imasleval  17497  issgrpd  18690  dfgrp3lem  19006  resscntz  19300  ablfac1c  20040  lbsind  21071  isphld  21630  mplcoe5lem  22016  cply1mul  22283  smadiadetr  22659  chfacfisf  22838  chfacfisfcpmat  22839  chcoeffeq  22870  cayhamlem3  22871  tx1stc  23634  ioorcl  25563  coemullem  26234  xrlimcnp  26951  fsumdvdscom  27167  fsumvma  27195  cusgrres  29536  usgredgsscusgredg  29547  clwlkclwwlklem2a  30087  clwwlkext2edg  30145  frgrwopreglem5ALT  30411  frgr2wwlkeu  30416  frgr2wwlk1  30418  grpoidinvlem3  30596  htthlem  31007  atcvat4i  32487  abfmpeld  32747  ressupprn  32783  isarchi3  33269  qsidomlem2  33537  ordtconnlem1  34117  gonarlem  35631  fmlasucdisj  35636  funpartfun  36180  relowlssretop  37734  ltflcei  37984  neificl  38129  keridl  38408  eqvrelth  39071  cvrat4  39944  ps-2  39979  mpaaeu  43604  clcnvlem  44076  fcoresf1  47540  modlt0b  47840  iccpartiltu  47905  2pwp1prm  48075  bgoldbtbnd  48308  isuspgrimlem  48394  grimedg  48434  grimgrtri  48448  lmod0rng  48728  lincext1  48953