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  3679  eqreu  3691  dedth3h  4539  prproe  4859  rbropap  5510  breldmg  5856  ssimaexg  6913  funopdmsn  7088  fpr3g  8225  wfr3g  8259  dfsmo2  8277  omwordri  8497  3ecoptocl  8743  ttrclselem2  9641  frr3g  9671  cfslb  10179  cofsmo  10182  cfsmolem  10183  coftr  10186  domtriomlem  10355  zorn2lem7  10415  ttukey2g  10429  gchi  10537  tskxpss  10685  tskord  10693  infm3  12102  uzind  12586  fzind  12592  fnn0ind  12593  xltnegi  13136  axdc4uz  13909  facwordi  14214  swrdnd2  14580  cshwidxmod  14727  relexpsucl  14956  relexpsucr  14957  relexprelg  14963  relexpaddnn  14976  caubnd  15284  mulgcd  16477  lcmfdvds  16571  lcmfdvdsb  16572  coprmdvds1  16581  pcfac  16829  ramz  16955  imasleval  17463  cictr  17730  initoeu2lem1  17939  drsdir  18226  psasym  18500  pstr  18501  tsrlin  18509  dirge  18527  mgmcl  18535  mgmhmlin  18591  issubmgm2  18595  mhmlin  18685  mhmmulg  19012  issubg2  19038  nsgbi  19054  gsumcom2  19872  srgmulgass  20120  dvdsrtr  20271  rnghmmul  20352  issubrng2  20461  issubrg2  20495  domnmuln0  20612  drnginvrcl  20656  drnginvrn0  20657  drnginvrl  20659  drnginvrr  20660  isdrngd  20668  isdrngdOLD  20670  abvmul  20724  abvtri  20725  lmhmlin  20957  ipcj  21559  cssincl  21613  obsip  21646  decpmatmulsumfsupp  22676  mp2pm2mplem4  22712  pm2mpghm  22719  pm2mpmhmlem1  22721  inopn  22802  basis1  22853  iscldtop  22998  2ndcdisj  23359  cnmpt2t  23576  cnmpt22  23577  cnmptcom  23581  fbasssin  23739  ptcmplem3  23957  xmeteq0  24242  prdsxmslem2  24433  nmvs  24580  nmolb  24621  volfiniun  25464  sincosq1sgn  26423  sincosq2sgn  26424  sincosq3sgn  26425  sincosq4sgn  26426  ssltsn  27721  addsproplem2  27900  negsproplem2  27958  negsid  27970  mulsproplem9  28050  precsexlem10  28141  uzsind  28316  recut  28383  0reno  28384  ewlkle  29569  wwlksnext  29856  umgr2adedgwlklem  29907  elwwlks2ons3im  29917  umgrwwlks2on  29920  conngrv2edg  30157  frgrwopregasn  30278  frgrwopregbsn  30279  frgrwopreglem5  30283  frgrwopreglem5ALT  30284  frgr2wwlkeu  30289  ablocom  30510  nmcvcn  30657  ipassi  30803  htth  30880  shaddcl  31179  shmulcl  31180  shsubcl  31182  chlimi  31196  pjspansn  31539  cnopc  31875  cnfnc  31892  adj1  31895  lnfnmul  32010  atord  32350  atcvat2  32351  cdj3i  32403  nexple  32802  signstfvc  34541  bnj910  34914  bnj1154  34965  umgr2cycllem  35112  pconncn  35196  mrsubccat  35490  shftvalg  35704  linethru  36126  sin2h  37589  cos2h  37590  tan2h  37591  dvasin  37683  areacirclem1  37687  riotasv  38937  lsmsatcv  38988  omllaw  39221  2llnjN  39546  dalawlem10  39859  dalawlem13  39862  dalawlem14  39863  pclfinclN  39929  ismrc  42674  fzsplit1nn0  42727  pell1234qrmulcl  42828  pell14qrmulcl  42836  onsucf1olem  43243  iunrelexp0  43675  bi23impib  44460  bi13impib  44461  trelded  44539  suctrALT  44799  suctrALTcf  44895  suctrALTcfVD  44896  stoweidlem17  45999  zm1nn  47287  bgoldbtbndlem4  47793  bgoldbtbnd  47794  tgblthelfgott  47800  vopnbgrelself  47840  clnbgr3stgrgrlic  48005  clcllaw  48176  ztprmneprm  48332  lcoel0  48414  linindslinci  48434  fv2arycl  48634