Theorem 3impib 1116

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 1110	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 1088

This theorem is referenced by:  3impia  1117  mob  3676  eqreu  3688  dedth3h  4536  prproe  4857  rbropap  5503  breldmg  5849  ssimaexg  6908  funopdmsn  7083  fpr3g  8215  wfr3g  8249  dfsmo2  8267  omwordri  8487  3ecoptocl  8733  ttrclselem2  9616  frr3g  9646  cfslb  10154  cofsmo  10157  cfsmolem  10158  coftr  10161  domtriomlem  10330  zorn2lem7  10390  ttukey2g  10404  gchi  10512  tskxpss  10660  tskord  10668  infm3  12078  uzind  12562  fzind  12568  fnn0ind  12569  xltnegi  13112  axdc4uz  13888  facwordi  14193  swrdnd2  14560  cshwidxmod  14707  relexpsucl  14935  relexpsucr  14936  relexprelg  14942  relexpaddnn  14955  caubnd  15263  mulgcd  16456  lcmfdvds  16550  lcmfdvdsb  16551  coprmdvds1  16560  pcfac  16808  ramz  16934  imasleval  17442  cictr  17709  initoeu2lem1  17918  drsdir  18205  psasym  18479  pstr  18480  tsrlin  18488  dirge  18506  mgmcl  18548  mgmhmlin  18604  issubmgm2  18608  mhmlin  18698  mhmmulg  19025  issubg2  19051  nsgbi  19067  gsumcom2  19885  srgmulgass  20133  dvdsrtr  20284  rnghmmul  20365  issubrng2  20471  issubrg2  20505  domnmuln0  20622  drnginvrcl  20666  drnginvrn0  20667  drnginvrl  20669  drnginvrr  20670  isdrngd  20678  isdrngdOLD  20680  abvmul  20734  abvtri  20735  lmhmlin  20967  ipcj  21569  cssincl  21623  obsip  21656  decpmatmulsumfsupp  22686  mp2pm2mplem4  22722  pm2mpghm  22729  pm2mpmhmlem1  22731  inopn  22812  basis1  22863  iscldtop  23008  2ndcdisj  23369  cnmpt2t  23586  cnmpt22  23587  cnmptcom  23591  fbasssin  23749  ptcmplem3  23967  xmeteq0  24251  prdsxmslem2  24442  nmvs  24589  nmolb  24630  volfiniun  25473  sincosq1sgn  26432  sincosq2sgn  26433  sincosq3sgn  26434  sincosq4sgn  26435  addsproplem2  27911  negsproplem2  27969  negsid  27981  mulsproplem9  28061  precsexlem10  28152  uzsind  28327  recut  28396  0reno  28397  ewlkle  29582  wwlksnext  29869  umgr2adedgwlklem  29920  elwwlks2ons3im  29930  umgrwwlks2on  29933  conngrv2edg  30170  frgrwopregasn  30291  frgrwopregbsn  30292  frgrwopreglem5  30296  frgrwopreglem5ALT  30297  frgr2wwlkeu  30302  ablocom  30523  nmcvcn  30670  ipassi  30816  htth  30893  shaddcl  31192  shmulcl  31193  shsubcl  31195  chlimi  31209  pjspansn  31552  cnopc  31888  cnfnc  31905  adj1  31908  lnfnmul  32023  atord  32363  atcvat2  32364  cdj3i  32416  nexple  32822  signstfvc  34582  bnj910  34955  bnj1154  35006  r1filimi  35106  umgr2cycllem  35172  pconncn  35256  mrsubccat  35550  shftvalg  35764  linethru  36186  sin2h  37649  cos2h  37650  tan2h  37651  dvasin  37743  areacirclem1  37747  riotasv  38997  lsmsatcv  39048  omllaw  39281  2llnjN  39605  dalawlem10  39918  dalawlem13  39921  dalawlem14  39922  pclfinclN  39988  ismrc  42733  fzsplit1nn0  42786  pell1234qrmulcl  42887  pell14qrmulcl  42895  onsucf1olem  43302  iunrelexp0  43734  bi23impib  44518  bi13impib  44519  trelded  44597  suctrALT  44857  suctrALTcf  44953  suctrALTcfVD  44954  stoweidlem17  46054  zm1nn  47332  bgoldbtbndlem4  47838  bgoldbtbnd  47839  tgblthelfgott  47845  vopnbgrelself  47885  clnbgr3stgrgrlic  48050  clcllaw  48221  ztprmneprm  48377  lcoel0  48459  linindslinci  48479  fv2arycl  48679