Theorem 3impib 1117

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)

Hypothesis

Ref	Expression
3impib.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
3impib	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impib

Step	Hyp	Ref	Expression
1		3impib.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 415	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1111	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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  df-3an 1089

This theorem is referenced by:  3impia  1118  mob  3723  eqreu  3735  dedth3h  4586  prproe  4905  rbropap  5570  breldmg  5920  ssimaexg  6995  funopdmsn  7170  fpr3g  8310  wfr3g  8347  dfsmo2  8387  omwordri  8610  3ecoptocl  8849  ttrclselem2  9766  frr3g  9796  cfslb  10306  cofsmo  10309  cfsmolem  10310  coftr  10313  domtriomlem  10482  zorn2lem7  10542  ttukey2g  10556  gchi  10664  tskxpss  10812  tskord  10820  infm3  12227  uzind  12710  fzind  12716  fnn0ind  12717  xltnegi  13258  axdc4uz  14025  facwordi  14328  swrdnd2  14693  cshwidxmod  14841  relexpsucl  15070  relexpsucr  15071  relexprelg  15077  relexpaddnn  15090  caubnd  15397  mulgcd  16585  lcmfdvds  16679  lcmfdvdsb  16680  coprmdvds1  16689  pcfac  16937  ramz  17063  imasleval  17586  cictr  17849  initoeu2lem1  18059  drsdir  18348  psasym  18621  pstr  18622  tsrlin  18630  dirge  18648  mgmcl  18656  mgmhmlin  18712  issubmgm2  18716  mhmlin  18806  mhmmulg  19133  issubg2  19159  nsgbi  19175  gsumcom2  19993  srgmulgass  20214  dvdsrtr  20368  rnghmmul  20449  issubrng2  20558  issubrg2  20592  domnmuln0  20709  drnginvrcl  20753  drnginvrn0  20754  drnginvrl  20756  drnginvrr  20757  isdrngd  20765  isdrngdOLD  20767  abvmul  20822  abvtri  20823  lmhmlin  21034  ipcj  21652  cssincl  21706  obsip  21741  decpmatmulsumfsupp  22779  mp2pm2mplem4  22815  pm2mpghm  22822  pm2mpmhmlem1  22824  inopn  22905  basis1  22957  iscldtop  23103  2ndcdisj  23464  cnmpt2t  23681  cnmpt22  23682  cnmptcom  23686  fbasssin  23844  ptcmplem3  24062  xmeteq0  24348  prdsxmslem2  24542  nmvs  24697  nmolb  24738  volfiniun  25582  sincosq1sgn  26540  sincosq2sgn  26541  sincosq3sgn  26542  sincosq4sgn  26543  ssltsn  27837  addsproplem2  28003  negsproplem2  28061  negsid  28073  mulsproplem9  28150  precsexlem10  28240  uzsind  28391  recut  28428  0reno  28429  ewlkle  29623  wwlksnext  29913  umgr2adedgwlklem  29964  elwwlks2ons3im  29974  umgrwwlks2on  29977  conngrv2edg  30214  frgrwopregasn  30335  frgrwopregbsn  30336  frgrwopreglem5  30340  frgrwopreglem5ALT  30341  frgr2wwlkeu  30346  ablocom  30567  nmcvcn  30714  ipassi  30860  htth  30937  shaddcl  31236  shmulcl  31237  shsubcl  31239  chlimi  31253  pjspansn  31596  cnopc  31932  cnfnc  31949  adj1  31952  lnfnmul  32067  atord  32407  atcvat2  32408  cdj3i  32460  nexple  32833  signstfvc  34589  bnj910  34962  bnj1154  35013  umgr2cycllem  35145  pconncn  35229  mrsubccat  35523  shftvalg  35732  linethru  36154  sin2h  37617  cos2h  37618  tan2h  37619  dvasin  37711  areacirclem1  37715  riotasv  38960  lsmsatcv  39011  omllaw  39244  2llnjN  39569  dalawlem10  39882  dalawlem13  39885  dalawlem14  39886  pclfinclN  39952  ismrc  42712  fzsplit1nn0  42765  pell1234qrmulcl  42866  pell14qrmulcl  42874  onsucf1olem  43283  iunrelexp0  43715  bi23impib  44506  bi13impib  44507  trelded  44585  suctrALT  44846  suctrALTcf  44942  suctrALTcfVD  44943  stoweidlem17  46032  zm1nn  47314  bgoldbtbndlem4  47795  bgoldbtbnd  47796  tgblthelfgott  47802  vopnbgrelself  47841  clnbgr3stgrgrlic  47979  clcllaw  48107  ztprmneprm  48263  lcoel0  48345  linindslinci  48365  fv2arycl  48569