Theorem 3impib 1113

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  3impia  1114  mob  3710  eqreu  3722  dedth3h  4583  prproe  4903  rbropap  5563  breldmg  5908  ssimaexg  6980  funopdmsn  7156  fpr3g  8292  wfr3g  8329  dfsmo2  8369  omwordri  8594  3ecoptocl  8830  ttrclselem2  9762  frr3g  9792  cfslb  10300  cofsmo  10303  cfsmolem  10304  coftr  10307  domtriomlem  10476  zorn2lem7  10536  ttukey2g  10550  gchi  10658  tskxpss  10806  tskord  10814  infm3  12219  uzind  12700  fzind  12706  fnn0ind  12707  xltnegi  13243  axdc4uz  13998  facwordi  14301  swrdnd2  14658  cshwidxmod  14806  relexpsucl  15031  relexpsucr  15032  relexprelg  15038  relexpaddnn  15051  caubnd  15358  mulgcd  16544  lcmfdvds  16638  lcmfdvdsb  16639  coprmdvds1  16648  pcfac  16896  ramz  17022  imasleval  17551  cictr  17816  initoeu2lem1  18031  drsdir  18322  psasym  18596  pstr  18597  tsrlin  18605  dirge  18623  mgmcl  18631  mgmhmlin  18687  issubmgm2  18691  mhmlin  18778  mhmmulg  19105  issubg2  19131  nsgbi  19147  gsumcom2  19969  srgmulgass  20196  dvdsrtr  20346  rnghmmul  20427  issubrng2  20536  issubrg2  20572  domnmuln0  20683  drnginvrcl  20727  drnginvrn0  20728  drnginvrl  20730  drnginvrr  20731  isdrngd  20739  isdrngdOLD  20741  abvmul  20796  abvtri  20797  lmhmlin  21009  ipcj  21626  cssincl  21680  obsip  21715  decpmatmulsumfsupp  22763  mp2pm2mplem4  22799  pm2mpghm  22806  pm2mpmhmlem1  22808  inopn  22889  basis1  22941  iscldtop  23087  2ndcdisj  23448  cnmpt2t  23665  cnmpt22  23666  cnmptcom  23670  fbasssin  23828  ptcmplem3  24046  xmeteq0  24332  prdsxmslem2  24526  nmvs  24681  nmolb  24722  volfiniun  25564  sincosq1sgn  26523  sincosq2sgn  26524  sincosq3sgn  26525  sincosq4sgn  26526  ssltsn  27819  addsproplem2  27981  negsproplem2  28035  negsid  28047  mulsproplem9  28122  precsexlem10  28212  recut  28344  0reno  28345  ewlkle  29539  wwlksnext  29824  umgr2adedgwlklem  29875  elwwlks2ons3im  29885  umgrwwlks2on  29888  conngrv2edg  30125  frgrwopregasn  30246  frgrwopregbsn  30247  frgrwopreglem5  30251  frgrwopreglem5ALT  30252  frgr2wwlkeu  30257  ablocom  30478  nmcvcn  30625  ipassi  30771  htth  30848  shaddcl  31147  shmulcl  31148  shsubcl  31150  chlimi  31164  pjspansn  31507  cnopc  31843  cnfnc  31860  adj1  31863  lnfnmul  31978  atord  32318  atcvat2  32319  cdj3i  32371  nexple  33855  signstfvc  34433  bnj910  34806  bnj1154  34857  umgr2cycllem  34981  pconncn  35065  mrsubccat  35359  shftvalg  35567  linethru  35990  sin2h  37324  cos2h  37325  tan2h  37326  dvasin  37418  areacirclem1  37422  riotasv  38670  lsmsatcv  38721  omllaw  38954  2llnjN  39279  dalawlem10  39592  dalawlem13  39595  dalawlem14  39596  pclfinclN  39662  ismrc  42395  fzsplit1nn0  42448  pell1234qrmulcl  42549  pell14qrmulcl  42557  onsucf1olem  42973  iunrelexp0  43406  bi23impib  44198  bi13impib  44199  trelded  44278  suctrALT  44539  suctrALTcf  44635  suctrALTcfVD  44636  stoweidlem17  45674  zm1nn  46951  bgoldbtbndlem4  47416  bgoldbtbnd  47417  tgblthelfgott  47423  vopnbgrelself  47458  clcllaw  47604  ztprmneprm  47762  lcoel0  47847  linindslinci  47867  fv2arycl  48072