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  3688  eqreu  3700  dedth3h  4549  prproe  4869  rbropap  5525  breldmg  5873  ssimaexg  6947  funopdmsn  7122  fpr3g  8264  wfr3g  8298  dfsmo2  8316  omwordri  8536  3ecoptocl  8782  ttrclselem2  9679  frr3g  9709  cfslb  10219  cofsmo  10222  cfsmolem  10223  coftr  10226  domtriomlem  10395  zorn2lem7  10455  ttukey2g  10469  gchi  10577  tskxpss  10725  tskord  10733  infm3  12142  uzind  12626  fzind  12632  fnn0ind  12633  xltnegi  13176  axdc4uz  13949  facwordi  14254  swrdnd2  14620  cshwidxmod  14768  relexpsucl  14997  relexpsucr  14998  relexprelg  15004  relexpaddnn  15017  caubnd  15325  mulgcd  16518  lcmfdvds  16612  lcmfdvdsb  16613  coprmdvds1  16622  pcfac  16870  ramz  16996  imasleval  17504  cictr  17767  initoeu2lem1  17976  drsdir  18263  psasym  18535  pstr  18536  tsrlin  18544  dirge  18562  mgmcl  18570  mgmhmlin  18626  issubmgm2  18630  mhmlin  18720  mhmmulg  19047  issubg2  19073  nsgbi  19089  gsumcom2  19905  srgmulgass  20126  dvdsrtr  20277  rnghmmul  20358  issubrng2  20467  issubrg2  20501  domnmuln0  20618  drnginvrcl  20662  drnginvrn0  20663  drnginvrl  20665  drnginvrr  20666  isdrngd  20674  isdrngdOLD  20676  abvmul  20730  abvtri  20731  lmhmlin  20942  ipcj  21543  cssincl  21597  obsip  21630  decpmatmulsumfsupp  22660  mp2pm2mplem4  22696  pm2mpghm  22703  pm2mpmhmlem1  22705  inopn  22786  basis1  22837  iscldtop  22982  2ndcdisj  23343  cnmpt2t  23560  cnmpt22  23561  cnmptcom  23565  fbasssin  23723  ptcmplem3  23941  xmeteq0  24226  prdsxmslem2  24417  nmvs  24564  nmolb  24605  volfiniun  25448  sincosq1sgn  26407  sincosq2sgn  26408  sincosq3sgn  26409  sincosq4sgn  26410  ssltsn  27704  addsproplem2  27877  negsproplem2  27935  negsid  27947  mulsproplem9  28027  precsexlem10  28118  uzsind  28293  recut  28347  0reno  28348  ewlkle  29533  wwlksnext  29823  umgr2adedgwlklem  29874  elwwlks2ons3im  29884  umgrwwlks2on  29887  conngrv2edg  30124  frgrwopregasn  30245  frgrwopregbsn  30246  frgrwopreglem5  30250  frgrwopreglem5ALT  30251  frgr2wwlkeu  30256  ablocom  30477  nmcvcn  30624  ipassi  30770  htth  30847  shaddcl  31146  shmulcl  31147  shsubcl  31149  chlimi  31163  pjspansn  31506  cnopc  31842  cnfnc  31859  adj1  31862  lnfnmul  31977  atord  32317  atcvat2  32318  cdj3i  32370  nexple  32769  signstfvc  34565  bnj910  34938  bnj1154  34989  umgr2cycllem  35127  pconncn  35211  mrsubccat  35505  shftvalg  35719  linethru  36141  sin2h  37604  cos2h  37605  tan2h  37606  dvasin  37698  areacirclem1  37702  riotasv  38952  lsmsatcv  39003  omllaw  39236  2llnjN  39561  dalawlem10  39874  dalawlem13  39877  dalawlem14  39878  pclfinclN  39944  ismrc  42689  fzsplit1nn0  42742  pell1234qrmulcl  42843  pell14qrmulcl  42851  onsucf1olem  43259  iunrelexp0  43691  bi23impib  44476  bi13impib  44477  trelded  44555  suctrALT  44815  suctrALTcf  44911  suctrALTcfVD  44912  stoweidlem17  46015  zm1nn  47303  bgoldbtbndlem4  47809  bgoldbtbnd  47810  tgblthelfgott  47816  vopnbgrelself  47855  clnbgr3stgrgrlic  48011  clcllaw  48179  ztprmneprm  48335  lcoel0  48417  linindslinci  48437  fv2arycl  48637