Theorem 3impia 1118

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 455	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1117	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  mopick2  2634  ceqsalt  3506  3gencl  3518  vtoclgft  3541  vtoclegft  3574  rspc6v  3631  mob2  3711  moi  3714  reupick3  4319  disjne  4454  elpr2elpr  4869  disji2  5130  disji  5131  tz7.2  5660  sofld  6184  ordintdif  6412  funopg  6580  fvun1  6980  fvopab6  7029  fveqressseq  7079  fvcofneq  7092  fprg  7150  2f1fvneq  7256  isores3  7329  ovmpt4g  7552  ovmpos  7553  ov2gf  7554  ofrval  7679  sorpssuni  7719  sorpssint  7720  poxp  8111  poseq  8141  suppss2  8182  frrlem12  8279  smoel  8357  smoord  8362  smogt  8364  oaass  8558  oewordi  8588  oeoalem  8593  oeoelem  8595  nnawordi  8618  nnaass  8619  naddssim  8681  qsel  8787  xpdom3  9067  onsdominel  9123  mapdom3  9146  sdomdomtrfi  9201  domsdomtrfi  9202  php  9207  onomeneq  9225  fisseneq  9254  cantnflem1  9681  ttrclss  9712  cfslbn  10259  cfsmolem  10262  cfcoflem  10264  infpssrlem4  10298  fin23lem7  10308  fin23lem25  10316  isf34lem7  10371  hsmexlem2  10419  axcc3  10430  axdc4lem  10447  tskss  10750  gruss  10788  gruurn  10790  gruiun  10791  gruel  10795  gruen  10804  grudomon  10809  grothac  10822  axpre-sup  11161  axsup  11286  addn0nid  11631  letrp1  12055  p1le  12056  lemul1a  12065  infrelb  12196  zextle  12632  zextlt  12633  btwnnz  12635  gtndiv  12636  uzind2  12652  fzind  12657  eluzsubOLD  12855  zsupss  12918  xrltne  13139  lemaxle  13171  qbtwnre  13175  qbtwnxr  13176  xlemul1a  13264  icogelb  13372  iccleub  13376  iccsplit  13459  uzsubsubfz  13520  elfz0fzfz0  13603  difelfznle  13612  fvffz0  13616  elfzo0le  13673  fzonmapblen  13675  fzofzim  13676  ceile  13811  modadd1  13870  muladdmodid  13873  modmul1  13886  modirr  13904  fsuppmapnn0fiub0  13955  expcl2lem  14036  expclzlem  14046  expnegz  14059  leexp2r  14136  bcval4  14264  bccmpl  14266  hashbnd  14293  hashunsnggt  14351  hashgt23el  14381  hashfundm  14399  elovmpowrd  14505  ccatval2  14525  ccatrcl1  14541  wrdl1s1  14561  ccat2s1fvw  14585  swrdsb0eq  14610  swrdccatin1  14672  pfxccatpfx2  14684  repswswrd  14731  cshwcsh2id  14776  absexpz  15249  climbdd  15615  iseraltlem2  15626  binomfallfac  15982  dvdsle  16250  divalgb  16344  ndvdssub  16349  dvdsgcd  16483  dfgcd2  16485  rplpwr  16496  lcmgcdlem  16540  lcmfunsn  16578  coprmdvds1  16586  qredeq  16591  2mulprm  16627  prmdvdsexpr  16651  nnnn0modprm0  16736  prm23ge5  16745  pcexp  16789  difsqpwdvds  16817  prmpwdvds  16834  ramcl  16959  cshwshashlem3  17028  cshwrepswhash1  17033  elrestr  17371  mreintcl  17536  mremre  17545  mrieqv2d  17580  initoeu2lem1  17961  funcestrcsetclem9  18097  funcsetcestrclem9  18112  prstr  18250  drsdirfi  18255  latnlej  18406  latnlej2  18409  acsdrsel  18493  acsdrscl  18496  mrelatglb  18510  mrelatlub  18512  isnmgm  18562  grpasscan1  18883  grpinvnz  18891  mulgneg2  18983  gsmsymgrfix  19291  f1omvdco2  19311  symggen  19333  odcl2  19428  odhash3  19439  lsmss1  19528  lsmss2  19530  efgred  19611  efgcpbl  19619  ablfacrp  19931  ablfac1eu  19938  ablfaclem3  19952  dvdsrmul1  20176  dvdsunit  20186  irredmul  20236  lmodlema  20469  psgnodpmr  21135  phlssphl  21204  lindsss  21371  lindfmm  21374  ply1scln0  21806  dmatelnd  21990  mdetdiaglem  22092  mdet0  22100  mdetunilem7  22112  slesolinv  22174  cramerimplem3  22179  cpmatpmat  22204  m2cpminvid2lem  22248  chfacfscmul0  22352  chfacfpmmul0  22356  riinopn  22402  clsndisj  22571  cnpf2  22746  hausnei2  22849  cmpcov  22885  cmpfii  22905  unconn  22925  t1connperf  22932  nrmr0reg  23245  fbfinnfr  23337  filuni  23381  alexsubALT  23547  tmdgsum  23591  cuspcvg  23798  mopni  23993  isngp4  24113  metdsre  24361  iimulcl  24445  phtpc01  24504  clmmulg  24609  cfilucfil4  24830  bcthlem5  24837  bcth  24838  bcth3  24840  itg1le  25223  itg2le  25249  bddmulibl  25348  bddiblnc  25351  dvnres  25440  cpnord  25444  dvnfre  25461  deg1ge  25608  dgr1term  25766  aaliou3lem2  25848  sincosq1lem  25999  cxpge0  26183  cxpmul2  26189  logrec  26258  logbgcd1irr  26289  sqfpc  26631  bcmono  26770  gausslemma2dlem1a  26858  gausslemma2dlem2  26860  gausslemma2dlem4  26862  2lgsoddprmlem3  26907  pntrmax  27057  qabvexp  27119  ostth2lem2  27127  nosepon  27158  nolesgn2o  27164  nogesgn1o  27166  nosepnelem  27172  nosepne  27173  nosepdmlem  27176  nosepdm  27177  nodenselem8  27184  noresle  27190  noetasuplem4  27229  noetainflem4  27233  scutbdaylt  27309  addsuniflem  27474  ssltmul1  27592  precsexlem6  27648  precsexlem7  27649  precsexlem11  27653  ax5seglem4  28180  axeuclidlem  28210  uhgredgrnv  28380  usgredg4  28464  nbuhgr2vtx1edgblem  28598  vtxduhgr0e  28725  vtxduhgr0nedg  28739  rusgrpropnb  28830  uspgr2wlkeqi  28895  redwlklem  28918  lfgrwlkprop  28934  2pthnloop  28978  spthonepeq  28999  pthdlem2lem  29014  crctcshwlkn0lem3  29056  crctcshwlkn0lem5  29058  crctcshwlkn0lem7  29060  crctcshwlkn0  29065  wlkiswwlks1  29111  wlkiswwlks2  29119  wlkiswwlksupgr2  29121  wwlksnext  29137  wwlksnextproplem2  29154  wspthsnonn0vne  29161  2pthon3v  29187  rusgrnumwwlk  29219  erclwwlkeqlen  29262  erclwwlksym  29264  erclwwlktr  29265  erclwwlkneqlen  29311  erclwwlknsym  29313  erclwwlkntr  29314  uhgr3cyclex  29425  upgreupthseg  29452  eupth2lem3lem4  29474  eucrctshift  29486  4cycl2vnunb  29533  nvs  29904  nvtri  29911  nmlno0  30036  nmlnoubi  30037  ubth  30114  hlipgt0  30155  ocnel  30539  elspansn2  30808  elspansn3  30813  normcan  30817  pjoml2  30852  lecm  30858  osum  30886  nmbdfnlb  31291  leopmul  31375  hstpyth  31470  cvnbtwn  31527  ssmd1  31552  ssmd2  31553  ssdmd1  31554  ssdmd2  31555  cvmd  31577  cvdmd  31578  superpos  31595  disji2f  31796  disjif  31797  disjif2  31800  preiman0  31919  padct  31932  ffs2  31941  bcm1n  31994  s2f1  32099  omndadd  32212  ogrpaddlt  32223  archiabl  32332  slmdlema  32336  lbslsat  32690  eulerpartlemb  33356  sgn3da  33529  fisshasheq  34093  cvmsdisj  34250  cvmlift2lem12  34294  satfrel  34347  satfrnmapom  34350  fmlasuc  34366  satffun  34389  satef  34396  sategoelfv  34400  lineintmo  35118  nn0prpwlem  35196  nn0prpw  35197  neibastop2lem  35234  lindsadd  36470  areacirc  36570  incsequz  36605  mettrifi  36614  ismtybnd  36664  heiborlem1  36668  rngoisocnv  36838  risci  36844  eqvrelqsel  37475  lfl1  37929  lkrlsp2  37962  omlfh3N  38118  cvrnbtwn  38130  cvrnbtwn2  38134  cvrnbtwn4  38138  cvlexch3  38191  cvlexch4N  38192  cvlatexchb1  38193  2llnne2N  38268  atcvrj0  38288  cvrat2  38289  ps-1  38337  3atlem5  38347  islln2a  38377  lplnriaN  38410  lplnribN  38411  llncvrlpln2  38417  lplncvrlvol2  38475  psubatN  38615  pmapglb2N  38631  pmapglb2xN  38632  2llnma1b  38646  paddasslem17  38696  pmod2iN  38709  pmodl42N  38711  hlmod1i  38716  atmod1i1  38717  atmod1i2  38719  llnmod1i2  38720  pclcmpatN  38761  osumcllem8N  38823  pexmidlem3N  38832  pl42lem4N  38842  4atexlem7  38935  ltrnnid  38996  cdlemc4  39054  cdleme32a  39301  cdlemeg46gfre  39392  cdlemf2  39422  cdlemg4c  39472  trlcoat  39583  tendovalco  39625  tendoeq2  39634  cdlemk36  39773  diael  39903  diatrl  39904  dicelval1stN  40048  dicelval2nd  40049  dihlspsnat  40193  dochkr1  40338  lcfrlem9  40410  mapdh8e  40644  hdmapval0  40693  hgmapval0  40752  nnadddir  41182  nn0rppwr  41220  nn0expgcd  41222  dvdsexpnn0  41228  incssnn0  41435  pell14qrexpcl  41591  pell14qrgap  41599  congadd  41691  acongsym  41701  acongtr  41703  dvdsacongtr  41709  jm2.19lem3  41716  jm2.19lem4  41717  jm2.26lem3  41726  onexlimgt  41978  nadd2rabex  42122  ismnushort  43046  bi13impia  43235  3impcombi  43564  ioogtlb  44195  iocgtlb  44202  iocleub  44203  icoltub  44208  iooltub  44210  limclner  44354  limsupre3lem  44435  climuzlem  44446  fsupdm  45545  finfdm  45549  elfzelfzlble  46016  subsubelfzo0  46021  iccpartigtl  46078  sqrtpwpw2p  46193  fmtnoprmfac1lem  46219  fmtno4prmfac  46227  evenltle  46372  even3prm2  46374  wtgoldbnnsum4prm  46457  bgoldbnnsum3prm  46459  bgoldbtbndlem1  46460  bgoldbtbndlem3  46462  bgoldbtbndlem4  46463  bgoldbtbnd  46464  upgrwlkupwlk  46505  c0snmgmhm  46699  funcringcsetcALTV2lem9  46896  funcringcsetclem9ALTV  46919  lincscmcl  47067  lindslinindimp2lem4  47096  lincresunit2  47113  lincresunit3  47116  elfzolborelfzop1  47154  m1modmmod  47161  rege1logbzge0  47199  fllog2  47208  dignn0ldlem  47242  rrx2pnecoorneor  47355  rrx2plord2  47362  rrx2linest  47382  ipolub  47567  ipoglb  47570