Theorem 3impib 1254

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 451	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1249	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  mob  3355  eqreu  3365  dedth3h  4091  rbropap  4940  breldmg  5252  ssimaexg  6174  wfr3g  7300  dfsmo2  7331  omwordri  7539  3ecoptocl  7726  cfslb  8971  cofsmo  8974  cfsmolem  8975  coftr  8978  domtriomlem  9147  zorn2lem7  9207  ttukey2g  9221  gchi  9325  tskxpss  9473  tskord  9481  infm3  10861  uzind  11345  fzind  11351  fnn0ind  11352  xltnegi  11921  axdc4uz  12645  facwordi  12938  swrdnd2  13285  cshwidxmod  13400  relexpsucr  13617  relexpsucl  13621  relexprelg  13626  relexpaddnn  13639  caubnd  13946  mulgcd  15103  lcmfdvds  15193  lcmfdvdsb  15194  coprmdvds1  15203  pcfac  15441  ramz  15567  imasleval  16024  cictr  16288  initoeu2lem1  16487  drsdir  16758  psasym  17033  pstr  17034  tsrlin  17042  dirge  17060  mgmcl  17068  mhmlin  17165  mhmmulg  17406  issubg2  17432  nsgbi  17448  cygabl  18115  gsumcom2  18197  srgmulgass  18354  dvdsrtr  18475  drnginvrcl  18587  drnginvrn0  18588  drnginvrl  18589  drnginvrr  18590  isdrngd  18595  issubrg2  18623  abvmul  18652  abvtri  18653  lmhmlin  18856  domnmuln0  19119  ipcj  19798  cssincl  19851  obsip  19884  decpmatmulsumfsupp  20397  mp2pm2mplem4  20433  pm2mpghm  20440  pm2mpmhmlem1  20442  inopn  20529  basis1  20565  iscldtop  20709  2ndcdisj  21069  cnmpt2t  21286  cnmpt22  21287  cnmptcom  21291  fbasssin  21450  ptcmplem3  21668  xmeteq0  21953  prdsxmslem2  22144  nmvs  22290  nmolb  22331  volfiniun  23122  sincosq1sgn  24054  sincosq2sgn  24055  sincosq3sgn  24056  sincosq4sgn  24057  usg2wlk  26145  wwlknext  26252  wwlkext2clwwlk  26331  cusgraisrusgra  26465  rusgra0edg  26482  numclwwlkovf2ex  26613  ablocom  26786  nmcvcn  26934  ipassi  27080  htth  27159  shaddcl  27458  shmulcl  27459  shsubcl  27461  chlimi  27475  pjspansn  27820  cnopc  28156  cnfnc  28173  adj1  28176  lnfnmul  28291  atord  28631  atcvat2  28632  cdj3i  28684  nexple  29399  signstfvc  29977  bnj910  30272  bnj1154  30321  pconcn  30460  mrsubccat  30669  shftvalg  30870  frr3g  31023  linethru  31430  sin2h  32569  cos2h  32570  tan2h  32571  dvasin  32666  areacirclem1  32670  riotasv  33263  lsmsatcv  33315  omllaw  33548  2llnjN  33871  dalawlem10  34184  dalawlem13  34187  dalawlem14  34188  pclfinclN  34254  ismrc  36282  fzsplit1nn0  36335  pell1234qrmulcl  36437  pell14qrmulcl  36445  iunrelexp0  37013  bi23impib  37712  bi13impib  37713  trelded  37802  suctrALT  38083  suctrALTcf  38180  suctrALTcfVD  38181  stoweidlem17  38910  bgoldbtbndlem4  40224  bgoldbtbnd  40225  tgblthelfgott  40229  tgblthelfgottOLD  40236  zm1nn  40348  ewlkle  40807  wwlksnext  41099  umgr2adedgwlklem  41151  elwwlks2ons3  41159  umgrwwlks2on  41161  wwlksext2clwwlk  41231  clwlksfclwwlk  41269  conngrv2edg  41362  av-numclwwlkovf2ex  41517  mgmhmlin  41576  issubmgm2  41580  clcllaw  41617  rnghmmul  41690  ztprmneprm  41918  lcoel0  42011  linindslinci  42031