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  3663  eqreu  3675  dedth3h  4527  prproe  4848  rbropap  5518  breldmg  5864  ssimaexg  6926  funopdmsn  7104  fpr3g  8235  wfr3g  8269  dfsmo2  8287  omwordri  8507  3ecoptocl  8756  ttrclselem2  9647  frr3g  9680  cfslb  10188  cofsmo  10191  cfsmolem  10192  coftr  10195  domtriomlem  10364  zorn2lem7  10424  ttukey2g  10438  gchi  10547  tskxpss  10695  tskord  10703  infm3  12115  uzind  12621  fzind  12627  fnn0ind  12628  xltnegi  13168  axdc4uz  13946  facwordi  14251  swrdnd2  14618  cshwidxmod  14765  relexpsucl  14993  relexpsucr  14994  relexprelg  15000  relexpaddnn  15013  caubnd  15321  mulgcd  16517  lcmfdvds  16611  lcmfdvdsb  16612  coprmdvds1  16621  pcfac  16870  ramz  16996  imasleval  17505  cictr  17772  initoeu2lem1  17981  drsdir  18268  psasym  18542  pstr  18543  tsrlin  18551  dirge  18569  mgmcl  18611  mgmhmlin  18667  issubmgm2  18671  mhmlin  18761  mhmmulg  19091  issubg2  19117  nsgbi  19132  gsumcom2  19950  srgmulgass  20198  dvdsrtr  20348  rnghmmul  20429  issubrng2  20535  issubrg2  20569  domnmuln0  20686  drnginvrcl  20730  drnginvrn0  20731  drnginvrl  20733  drnginvrr  20734  isdrngd  20742  isdrngdOLD  20744  abvmul  20798  abvtri  20799  lmhmlin  21030  ipcj  21614  cssincl  21668  obsip  21701  decpmatmulsumfsupp  22738  mp2pm2mplem4  22774  pm2mpghm  22781  pm2mpmhmlem1  22783  inopn  22864  basis1  22915  iscldtop  23060  2ndcdisj  23421  cnmpt2t  23638  cnmpt22  23639  cnmptcom  23643  fbasssin  23801  ptcmplem3  24019  xmeteq0  24303  prdsxmslem2  24494  nmvs  24641  nmolb  24682  volfiniun  25514  sincosq1sgn  26462  sincosq2sgn  26463  sincosq3sgn  26464  sincosq4sgn  26465  addsproplem2  27962  negsproplem2  28021  negsid  28033  mulsproplem9  28116  precsexlem10  28208  uzsind  28397  recut  28486  ewlkle  29674  wwlksnext  29961  umgr2adedgwlklem  30012  elwwlks2ons3im  30022  usgrwwlks2on  30026  umgrwwlks2on  30027  conngrv2edg  30265  frgrwopregasn  30386  frgrwopregbsn  30387  frgrwopreglem5  30391  frgrwopreglem5ALT  30392  frgr2wwlkeu  30397  ablocom  30619  nmcvcn  30766  ipassi  30912  htth  30989  shaddcl  31288  shmulcl  31289  shsubcl  31291  chlimi  31305  pjspansn  31648  cnopc  31984  cnfnc  32001  adj1  32004  lnfnmul  32119  atord  32459  atcvat2  32460  cdj3i  32512  nexple  32917  signstfvc  34718  bnj910  35090  bnj1154  35141  r1filimi  35246  umgr2cycllem  35322  pconncn  35406  mrsubccat  35700  shftvalg  35914  linethru  36335  sin2h  37931  cos2h  37932  tan2h  37933  dvasin  38025  areacirclem1  38029  riotasv  39405  lsmsatcv  39456  omllaw  39689  2llnjN  40013  dalawlem10  40326  dalawlem13  40329  dalawlem14  40330  pclfinclN  40396  ismrc  43133  fzsplit1nn0  43186  pell1234qrmulcl  43283  pell14qrmulcl  43291  onsucf1olem  43698  iunrelexp0  44129  bi23impib  44913  bi13impib  44914  trelded  44992  suctrALT  45252  suctrALTcf  45348  suctrALTcfVD  45349  stoweidlem17  46445  zm1nn  47750  bgoldbtbndlem4  48284  bgoldbtbnd  48285  tgblthelfgott  48291  vopnbgrelself  48331  clnbgr3stgrgrlic  48496  clcllaw  48667  ztprmneprm  48823  lcoel0  48904  linindslinci  48924  fv2arycl  49124