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  3664  eqreu  3676  dedth3h  4528  prproe  4849  rbropap  5511  breldmg  5858  ssimaexg  6920  funopdmsn  7097  fpr3g  8228  wfr3g  8262  dfsmo2  8280  omwordri  8500  3ecoptocl  8749  ttrclselem2  9638  frr3g  9671  cfslb  10179  cofsmo  10182  cfsmolem  10183  coftr  10186  domtriomlem  10355  zorn2lem7  10415  ttukey2g  10429  gchi  10538  tskxpss  10686  tskord  10694  infm3  12106  uzind  12612  fzind  12618  fnn0ind  12619  xltnegi  13159  axdc4uz  13937  facwordi  14242  swrdnd2  14609  cshwidxmod  14756  relexpsucl  14984  relexpsucr  14985  relexprelg  14991  relexpaddnn  15004  caubnd  15312  mulgcd  16508  lcmfdvds  16602  lcmfdvdsb  16603  coprmdvds1  16612  pcfac  16861  ramz  16987  imasleval  17496  cictr  17763  initoeu2lem1  17972  drsdir  18259  psasym  18533  pstr  18534  tsrlin  18542  dirge  18560  mgmcl  18602  mgmhmlin  18658  issubmgm2  18662  mhmlin  18752  mhmmulg  19082  issubg2  19108  nsgbi  19123  gsumcom2  19941  srgmulgass  20189  dvdsrtr  20339  rnghmmul  20420  issubrng2  20526  issubrg2  20560  domnmuln0  20677  drnginvrcl  20721  drnginvrn0  20722  drnginvrl  20724  drnginvrr  20725  isdrngd  20733  isdrngdOLD  20735  abvmul  20789  abvtri  20790  lmhmlin  21022  ipcj  21624  cssincl  21678  obsip  21711  decpmatmulsumfsupp  22748  mp2pm2mplem4  22784  pm2mpghm  22791  pm2mpmhmlem1  22793  inopn  22874  basis1  22925  iscldtop  23070  2ndcdisj  23431  cnmpt2t  23648  cnmpt22  23649  cnmptcom  23653  fbasssin  23811  ptcmplem3  24029  xmeteq0  24313  prdsxmslem2  24504  nmvs  24651  nmolb  24692  volfiniun  25524  sincosq1sgn  26475  sincosq2sgn  26476  sincosq3sgn  26477  sincosq4sgn  26478  addsproplem2  27976  negsproplem2  28035  negsid  28047  mulsproplem9  28130  precsexlem10  28222  uzsind  28411  recut  28500  ewlkle  29689  wwlksnext  29976  umgr2adedgwlklem  30027  elwwlks2ons3im  30037  usgrwwlks2on  30041  umgrwwlks2on  30042  conngrv2edg  30280  frgrwopregasn  30401  frgrwopregbsn  30402  frgrwopreglem5  30406  frgrwopreglem5ALT  30407  frgr2wwlkeu  30412  ablocom  30634  nmcvcn  30781  ipassi  30927  htth  31004  shaddcl  31303  shmulcl  31304  shsubcl  31306  chlimi  31320  pjspansn  31663  cnopc  31999  cnfnc  32016  adj1  32019  lnfnmul  32134  atord  32474  atcvat2  32475  cdj3i  32527  nexple  32932  signstfvc  34734  bnj910  35106  bnj1154  35157  r1filimi  35262  umgr2cycllem  35338  pconncn  35422  mrsubccat  35716  shftvalg  35930  linethru  36351  sin2h  37945  cos2h  37946  tan2h  37947  dvasin  38039  areacirclem1  38043  riotasv  39419  lsmsatcv  39470  omllaw  39703  2llnjN  40027  dalawlem10  40340  dalawlem13  40343  dalawlem14  40344  pclfinclN  40410  ismrc  43147  fzsplit1nn0  43200  pell1234qrmulcl  43301  pell14qrmulcl  43309  onsucf1olem  43716  iunrelexp0  44147  bi23impib  44931  bi13impib  44932  trelded  45010  suctrALT  45270  suctrALTcf  45366  suctrALTcfVD  45367  stoweidlem17  46463  zm1nn  47762  bgoldbtbndlem4  48296  bgoldbtbnd  48297  tgblthelfgott  48303  vopnbgrelself  48343  clnbgr3stgrgrlic  48508  clcllaw  48679  ztprmneprm  48835  lcoel0  48916  linindslinci  48936  fv2arycl  49136