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  3815  csbie2t  3885  frinxp  5705  ordelord  6337  foco2  7052  f1ounsn  7216  frxp  8066  mpocurryd  8209  omsmolem  8583  erth  8687  unblem1  9190  unwdomg  9487  cflim2  10171  distrlem1pr  10934  uz11  12774  elpq  12886  xmulge0  13197  max0add  15231  lcmfunsnlem2lem1  16563  divgcdcoprm0  16590  cncongr1  16592  prmpwdvds  16830  imasleval  17460  issgrpd  18653  dfgrp3lem  18966  resscntz  19260  ablfac1c  20000  lbsind  21030  isphld  21607  mplcoe5lem  21992  cply1mul  22238  smadiadetr  22617  chfacfisf  22796  chfacfisfcpmat  22797  chcoeffeq  22828  cayhamlem3  22829  tx1stc  23592  ioorcl  25532  coemullem  26209  xrlimcnp  26932  fsumdvdscom  27149  fsumvma  27178  cusgrres  29471  usgredgsscusgredg  29482  clwlkclwwlklem2a  30022  clwwlkext2edg  30080  frgrwopreglem5ALT  30346  frgr2wwlkeu  30351  frgr2wwlk1  30353  grpoidinvlem3  30530  htthlem  30941  atcvat4i  32421  abfmpeld  32681  ressupprn  32718  isarchi3  33218  qsidomlem2  33483  ordtconnlem1  34030  gonarlem  35537  fmlasucdisj  35542  funpartfun  36086  relowlssretop  37507  ltflcei  37748  neificl  37893  keridl  38172  eqvrelth  38807  cvrat4  39642  ps-2  39677  mpaaeu  43334  clcnvlem  43806  fcoresf1  47257  modlt0b  47551  iccpartiltu  47610  2pwp1prm  47777  bgoldbtbnd  47997  isuspgrimlem  48083  grimedg  48123  grimgrtri  48137  lmod0rng  48417  lincext1  48642