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  3700  eqreu  3712  dedth3h  4561  prproe  4881  rbropap  5540  breldmg  5889  ssimaexg  6965  funopdmsn  7140  fpr3g  8284  wfr3g  8321  dfsmo2  8361  omwordri  8584  3ecoptocl  8823  ttrclselem2  9740  frr3g  9770  cfslb  10280  cofsmo  10283  cfsmolem  10284  coftr  10287  domtriomlem  10456  zorn2lem7  10516  ttukey2g  10530  gchi  10638  tskxpss  10786  tskord  10794  infm3  12201  uzind  12685  fzind  12691  fnn0ind  12692  xltnegi  13232  axdc4uz  14002  facwordi  14307  swrdnd2  14673  cshwidxmod  14821  relexpsucl  15050  relexpsucr  15051  relexprelg  15057  relexpaddnn  15070  caubnd  15377  mulgcd  16567  lcmfdvds  16661  lcmfdvdsb  16662  coprmdvds1  16671  pcfac  16919  ramz  17045  imasleval  17555  cictr  17818  initoeu2lem1  18027  drsdir  18314  psasym  18586  pstr  18587  tsrlin  18595  dirge  18613  mgmcl  18621  mgmhmlin  18677  issubmgm2  18681  mhmlin  18771  mhmmulg  19098  issubg2  19124  nsgbi  19140  gsumcom2  19956  srgmulgass  20177  dvdsrtr  20328  rnghmmul  20409  issubrng2  20518  issubrg2  20552  domnmuln0  20669  drnginvrcl  20713  drnginvrn0  20714  drnginvrl  20716  drnginvrr  20717  isdrngd  20725  isdrngdOLD  20727  abvmul  20781  abvtri  20782  lmhmlin  20993  ipcj  21594  cssincl  21648  obsip  21681  decpmatmulsumfsupp  22711  mp2pm2mplem4  22747  pm2mpghm  22754  pm2mpmhmlem1  22756  inopn  22837  basis1  22888  iscldtop  23033  2ndcdisj  23394  cnmpt2t  23611  cnmpt22  23612  cnmptcom  23616  fbasssin  23774  ptcmplem3  23992  xmeteq0  24277  prdsxmslem2  24468  nmvs  24615  nmolb  24656  volfiniun  25500  sincosq1sgn  26459  sincosq2sgn  26460  sincosq3sgn  26461  sincosq4sgn  26462  ssltsn  27756  addsproplem2  27929  negsproplem2  27987  negsid  27999  mulsproplem9  28079  precsexlem10  28170  uzsind  28345  recut  28399  0reno  28400  ewlkle  29585  wwlksnext  29875  umgr2adedgwlklem  29926  elwwlks2ons3im  29936  umgrwwlks2on  29939  conngrv2edg  30176  frgrwopregasn  30297  frgrwopregbsn  30298  frgrwopreglem5  30302  frgrwopreglem5ALT  30303  frgr2wwlkeu  30308  ablocom  30529  nmcvcn  30676  ipassi  30822  htth  30899  shaddcl  31198  shmulcl  31199  shsubcl  31201  chlimi  31215  pjspansn  31558  cnopc  31894  cnfnc  31911  adj1  31914  lnfnmul  32029  atord  32369  atcvat2  32370  cdj3i  32422  nexple  32823  signstfvc  34606  bnj910  34979  bnj1154  35030  umgr2cycllem  35162  pconncn  35246  mrsubccat  35540  shftvalg  35749  linethru  36171  sin2h  37634  cos2h  37635  tan2h  37636  dvasin  37728  areacirclem1  37732  riotasv  38977  lsmsatcv  39028  omllaw  39261  2llnjN  39586  dalawlem10  39899  dalawlem13  39902  dalawlem14  39903  pclfinclN  39969  ismrc  42724  fzsplit1nn0  42777  pell1234qrmulcl  42878  pell14qrmulcl  42886  onsucf1olem  43294  iunrelexp0  43726  bi23impib  44511  bi13impib  44512  trelded  44590  suctrALT  44850  suctrALTcf  44946  suctrALTcfVD  44947  stoweidlem17  46046  zm1nn  47331  bgoldbtbndlem4  47822  bgoldbtbnd  47823  tgblthelfgott  47829  vopnbgrelself  47868  clnbgr3stgrgrlic  48024  clcllaw  48166  ztprmneprm  48322  lcoel0  48404  linindslinci  48424  fv2arycl  48628