Theorem 3impia 1138

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Hypothesis

Ref	Expression
3impia.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
3impia	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	expimpd 443	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1137	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  mopick2  2704  3gencl  3431  vtoclgft  3448  mob2  3584  moi  3587  reupick3  4113  disjne  4219  elpr2elpr  4591  disji2  4828  disji  4829  tz7.2  5295  sofld  5792  ordintdif  5987  funopg  6135  fvun1  6490  fvopab6  6532  fveqressseq  6577  fvcofneq  6589  fprg  6646  2f1fvneq  6741  isores3  6809  ovmpt4g  7013  ovmpt2s  7014  ov2gf  7015  ofrval  7137  sorpssuni  7176  sorpssint  7177  poxp  7523  suppss2  7564  smoel  7693  smoord  7698  smogt  7700  oaass  7878  oewordi  7908  oeoalem  7913  oeoelem  7915  nnawordi  7938  nnaass  7939  qsel  8061  xpdom3  8297  onsdominel  8348  mapdom3  8371  fisseneq  8410  cantnflem1  8833  cfslbn  9374  cfsmolem  9377  cfcoflem  9379  infpssrlem4  9413  fin23lem7  9423  fin23lem25  9431  isf34lem7  9486  hsmexlem2  9534  axcc3  9545  axdc4lem  9562  tskss  9865  gruss  9903  gruurn  9905  gruiun  9906  gruel  9910  gruen  9919  grudomon  9924  grothac  9937  axpre-sup  10275  axsup  10398  addn0nid  10736  letrp1  11150  p1le  11151  lemul1a  11162  infrelb  11293  zextle  11716  zextlt  11717  btwnnz  11719  gtndiv  11720  uzind2  11736  fzind  11741  eluzsub  11934  zsupss  11996  xrltne  12212  lemaxle  12244  qbtwnre  12248  qbtwnxr  12249  xlemul1a  12336  icogelb  12443  iccleub  12447  iccsplit  12528  uzsubsubfz  12586  elfz0fzfz0  12668  difelfznle  12677  fvffz0  12681  elfzo0le  12736  fzonmapblen  12738  fzofzim  12739  ceile  12872  modadd1  12931  muladdmodid  12934  modmul1  12947  modirr  12965  fsuppmapnn0fiub0  13016  expcl2lem  13095  expclzlem  13107  expnegz  13117  leexp2r  13141  bcval4  13314  bccmpl  13316  hashbnd  13343  elovmpt2wrd  13559  ccatval2  13575  ccatrcl1  13591  wrdl1s1  13609  ccat2s1fvw  13638  swrdsb0eq  13671  swrdccatin1  13707  repswswrd  13755  cshwcsh2id  13798  absexpz  14268  climbdd  14625  iseraltlem2  14636  binomfallfac  14992  dvdsle  15255  divalgb  15347  ndvdssub  15352  dvdsgcd  15480  rplpwr  15495  lcmgcdlem  15538  lcmfunsn  15576  coprmdvds1  15584  qredeq  15589  prmdvdsexpr  15646  nnnn0modprm0  15728  prm23ge5  15737  pcexp  15781  difsqpwdvds  15808  prmpwdvds  15825  ramcl  15950  cshwshashlem3  16016  cshwrepswhash1  16021  elrestr  16294  xpscfv  16427  mreintcl  16460  mremre  16469  mrieqv2d  16504  initoeu2lem1  16868  funcestrcsetclem9  16993  funcsetcestrclem9  17008  prstr  17138  drsdirfi  17143  latnlej  17273  latnlej2  17276  acsdrsel  17372  acsdrscl  17375  mrelatglb  17389  mrelatlub  17391  isnmgm  17451  grpasscan1  17683  grpinvnz  17691  mulgneg2  17778  gsmsymgrfix  18049  f1omvdco2  18069  symggen  18091  odcl2  18183  odhash3  18192  lsmss1  18280  lsmss2  18282  efgred  18362  efgcpbl  18370  ablfacrp  18667  ablfac1eu  18674  ablfaclem3  18688  dvdsrmul1  18855  dvdsunit  18865  irredmul  18911  lmodlema  19072  ply1scln0  19869  psgnodpmr  20143  lindsss  20373  lindfmm  20376  dmatelnd  20513  mdetdiaglem  20615  mdet0  20623  mdetunilem7  20635  slesolinv  20698  cramerimplem3  20704  cpmatpmat  20728  m2cpminvid2lem  20772  chfacfscmul0  20876  chfacfpmmul0  20880  riinopn  20926  clsndisj  21093  cnpf2  21268  hausnei2  21371  cmpcov  21406  cmpfii  21426  unconn  21446  t1connperf  21453  nrmr0reg  21766  fbfinnfr  21858  filuni  21902  alexsubALT  22068  tmdgsum  22112  cuspcvg  22318  mopni  22510  isngp4  22629  metdsre  22869  iimulcl  22949  phtpc01  23008  clmmulg  23113  cfilucfil4  23330  bcthlem5  23337  bcth  23338  bcth3  23340  itg1le  23694  itg2le  23720  bddmulibl  23819  dvnres  23908  cpnord  23912  dvnfre  23929  deg1ge  24072  dgr1term  24230  aaliou3lem2  24312  sincosq1lem  24464  cxpge0  24643  cxpmul2  24649  logrec  24715  sqfpc  25077  bcmono  25216  gausslemma2dlem1a  25304  gausslemma2dlem2  25306  gausslemma2dlem4  25308  2lgsoddprmlem3  25353  pntrmax  25467  qabvexp  25529  ostth2lem2  25537  ax5seglem4  26026  axeuclidlem  26056  uhgredgrnv  26239  usgredg4  26324  nbuhgr2vtx1edgblem  26463  vtxduhgr0e  26602  vtxduhgr0nedg  26616  rusgrpropnb  26707  uspgr2wlkeqi  26772  redwlklem  26796  lfgrwlkprop  26812  2pthnloop  26855  spthonepeq  26876  pthdlem2lem  26891  crctcshwlkn0lem3  26933  crctcshwlkn0lem5  26935  crctcshwlkn0lem7  26937  crctcshwlkn0  26942  wlkiswwlks1  26994  wlkiswwlks2  27002  wlkiswwlksupgr2  27004  wwlksnext  27030  wwlksnextproplem2  27048  wspthsnonn0vne  27057  2pthon3v  27083  rusgrnumwwlk  27117  erclwwlkeqlen  27162  erclwwlksym  27164  erclwwlktr  27165  wwlksext2clwwlkOLD  27208  erclwwlkneqlen  27219  erclwwlknsym  27221  erclwwlkntr  27222  uhgr3cyclex  27355  upgreupthseg  27382  eupth2lem3lem4  27404  eucrctshift  27416  4cycl2vnunb  27465  nvs  27846  nvtri  27853  nmlno0  27978  nmlnoubi  27979  ubth  28057  hlipgt0  28098  ocnel  28485  elspansn2  28754  elspansn3  28759  normcan  28763  pjoml2  28798  lecm  28804  osum  28832  nmbdfnlb  29237  leopmul  29321  hstpyth  29416  cvnbtwn  29473  ssmd1  29498  ssmd2  29499  ssdmd1  29500  ssdmd2  29501  cvmd  29523  cvdmd  29524  superpos  29541  disji2f  29715  disjif  29716  disjif2  29719  padct  29824  ffs2  29830  bcm1n  29881  omndadd  30031  ogrpaddlt  30043  archiabl  30077  slmdlema  30081  eulerpartlemb  30755  sgn3da  30928  cvmsdisj  31575  cvmlift2lem12  31619  br1steqgOLD  31994  br2ndeqgOLD  31995  poseq  32074  nosepon  32139  nolesgn2o  32145  nosepnelem  32151  nosepne  32152  nosepdmlem  32154  nosepdm  32155  nodenselem8  32162  noresle  32167  noetalem3  32186  sslttr  32235  scutbdaylt  32243  lineintmo  32585  nn0prpwlem  32638  nn0prpw  32639  neibastop2lem  32676  bddiblnc  33792  areacirc  33817  incsequz  33855  mettrifi  33864  ismtybnd  33917  heiborlem1  33921  rngoisocnv  34091  risci  34097  lfl1  34850  lkrlsp2  34883  omlfh3N  35039  cvrnbtwn  35051  cvrnbtwn2  35055  cvrnbtwn4  35059  cvlexch3  35112  cvlexch4N  35113  cvlatexchb1  35114  2llnne2N  35188  atcvrj0  35208  cvrat2  35209  ps-1  35257  3atlem5  35267  islln2a  35297  lplnriaN  35330  lplnribN  35331  llncvrlpln2  35337  lplncvrlvol2  35395  psubatN  35535  pmapglb2N  35551  pmapglb2xN  35552  2llnma1b  35566  paddasslem17  35616  pmod2iN  35629  pmodl42N  35631  hlmod1i  35636  atmod1i1  35637  atmod1i2  35639  llnmod1i2  35640  pclcmpatN  35681  osumcllem8N  35743  pexmidlem3N  35752  pl42lem4N  35762  4atexlem7  35855  ltrnnid  35916  cdlemc4  35975  cdleme32a  36222  cdlemeg46gfre  36313  cdlemf2  36343  cdlemg4c  36393  trlcoat  36504  tendovalco  36546  tendoeq2  36555  cdlemk36  36694  diael  36824  diatrl  36825  dicelval1stN  36969  dicelval2nd  36970  dihlspsnat  37114  dochkr1  37259  lcfrlem9  37331  mapdh8e  37565  hdmapval0  37614  hgmapval0  37673  incssnn0  37776  pell14qrexpcl  37933  pell14qrgap  37941  congadd  38034  acongsym  38044  acongtr  38046  dvdsacongtr  38052  jm2.19lem3  38059  jm2.19lem4  38060  jm2.26lem3  38069  relexpiidm  38496  bi13impia  39192  3impcombi  39541  ioogtlb  40201  iocgtlb  40208  iocleub  40209  icoltub  40215  iooltub  40217  limclner  40363  limsupre3lem  40444  climuzlem  40455  elfzelfzlble  41906  subsubelfzo0  41911  iccpartigtl  41934  pfx2  41987  pfxccatpfx2  42003  sqrtpwpw2p  42025  fmtnoprmfac1lem  42051  fmtno4prmfac  42059  evenltle  42201  even3prm2  42203  wtgoldbnnsum4prm  42265  bgoldbnnsum3prm  42267  bgoldbtbndlem1  42268  bgoldbtbndlem3  42270  bgoldbtbndlem4  42271  bgoldbtbnd  42272  upgrwlkupwlk  42289  c0snmgmhm  42482  funcringcsetcALTV2lem9  42612  funcringcsetclem9ALTV  42635  lincscmcl  42789  lindslinindimp2lem4  42818  lincresunit2  42835  lincresunit3  42838  elfzolborelfzop1  42877  m1modmmod  42884  rege1logbzge0  42921  fllog2  42930  dignn0ldlem  42964