Theorem 3impia 1117

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 453	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1116	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:  mopick2  2637  ceqsalt  3499  3gencl  3509  vtoclgft  3536  vtoclegft  3572  rspc6v  3627  mob2  3703  moi  3706  reupick3  4310  disjne  4435  elpr2elpr  4850  disji2  5108  disji  5109  tz7.2  5642  sofld  6181  ordintdif  6408  funopg  6575  fvun1  6975  fvopab6  7025  fveqressseq  7074  fvcofneq  7088  fprg  7150  isores3  7333  ovmpt4g  7559  ovmpos  7560  ov2gf  7561  ofrval  7688  sorpssuni  7731  sorpssint  7732  poxp  8132  poseq  8162  suppss2  8204  frrlem12  8301  smoel  8379  smoord  8384  smogt  8386  oaass  8578  oewordi  8608  oeoalem  8613  oeoelem  8615  nnawordi  8638  nnaass  8639  naddssim  8702  qsel  8815  xpdom3  9089  onsdominel  9145  mapdom3  9168  sdomdomtrfi  9220  domsdomtrfi  9221  php  9226  onomeneq  9242  fisseneq  9270  fodomfir  9345  cantnflem1  9708  ttrclss  9739  cfslbn  10286  cfsmolem  10289  cfcoflem  10291  infpssrlem4  10325  fin23lem7  10335  fin23lem25  10343  isf34lem7  10398  hsmexlem2  10446  axcc3  10457  axdc4lem  10474  tskss  10777  gruss  10815  gruurn  10817  gruiun  10818  gruel  10822  gruen  10831  grudomon  10836  grothac  10849  axpre-sup  11188  axsup  11315  addn0nid  11662  letrp1  12090  p1le  12091  lemul1a  12100  infrelb  12232  zextle  12671  zextlt  12672  btwnnz  12674  gtndiv  12675  uzind2  12691  fzind  12696  eluzsubOLD  12893  zsupss  12958  xrltne  13184  lemaxle  13216  qbtwnre  13220  qbtwnxr  13221  xlemul1a  13309  icogelb  13418  iccleub  13423  iccsplit  13507  uzsubsubfz  13568  elfz0fzfz0  13655  difelfznle  13664  fvffz0  13668  elfzo0le  13725  fzonmapblen  13730  fzofzim  13731  ceile  13871  modadd1  13930  muladdmodid  13933  modmul1  13947  modirr  13965  fsuppmapnn0fiub0  14016  expcl2lem  14096  expclzlem  14106  expnegz  14119  leexp2r  14197  bcval4  14330  bccmpl  14332  hashbnd  14359  hashunsnggt  14417  hashgt23el  14447  hashfundm  14465  elovmpowrd  14581  ccatval2  14601  ccatrcl1  14617  wrdl1s1  14637  ccat2s1fvw  14661  swrdsb0eq  14686  swrdccatin1  14748  pfxccatpfx2  14760  repswswrd  14807  cshwcsh2id  14852  absexpz  15329  climbdd  15693  iseraltlem2  15704  binomfallfac  16062  dvdsle  16334  divalgb  16428  ndvdssub  16433  dvdsgcd  16568  dfgcd2  16570  rplpwr  16582  nn0rppwr  16585  nn0expgcd  16588  lcmgcdlem  16630  lcmfunsn  16668  coprmdvds1  16676  qredeq  16681  2mulprm  16717  prmdvdsexpr  16741  nnnn0modprm0  16831  prm23ge5  16840  pcexp  16884  difsqpwdvds  16912  prmpwdvds  16929  ramcl  17054  cshwshashlem3  17122  cshwrepswhash1  17127  elrestr  17447  mreintcl  17612  mremre  17621  mrieqv2d  17656  initoeu2lem1  18032  funcestrcsetclem9  18165  funcsetcestrclem9  18180  prstr  18316  drsdirfi  18322  latnlej  18471  latnlej2  18474  acsdrsel  18558  acsdrscl  18561  mrelatglb  18575  mrelatlub  18577  isnmgm  18627  grpasscan1  18989  grpinvnz  18998  mulgneg2  19096  gsmsymgrfix  19414  f1omvdco2  19434  symggen  19456  odcl2  19551  odhash3  19562  lsmss1  19651  lsmss2  19653  efgred  19734  efgcpbl  19742  ablfacrp  20054  ablfac1eu  20061  ablfaclem3  20075  dvdsrmul1  20334  dvdsunit  20344  irredmul  20394  c0snmgmhm  20427  lmodlema  20827  psgnodpmr  21555  phlssphl  21624  lindsss  21789  lindfmm  21792  ply1scln0  22234  dmatelnd  22439  mdetdiaglem  22541  mdet0  22549  mdetunilem7  22561  slesolinv  22623  cramerimplem3  22628  cpmatpmat  22653  m2cpminvid2lem  22697  chfacfscmul0  22801  chfacfpmmul0  22805  riinopn  22851  clsndisj  23018  cnpf2  23193  hausnei2  23296  cmpcov  23332  cmpfii  23352  unconn  23372  t1connperf  23379  nrmr0reg  23692  fbfinnfr  23784  filuni  23828  alexsubALT  23994  tmdgsum  24038  cuspcvg  24244  mopni  24436  isngp4  24556  metdsre  24798  iimulcl  24889  phtpc01  24951  clmmulg  25057  cfilucfil4  25278  bcthlem5  25285  bcth  25286  bcth3  25288  itg1le  25671  itg2le  25697  bddmulibl  25797  bddiblnc  25800  dvnres  25890  cpnord  25894  dvnfre  25913  deg1ge  26060  dgr1term  26222  aaliou3lem2  26308  sincosq1lem  26463  cxpge0  26649  cxpmul2  26655  logrec  26730  logbgcd1irr  26761  sqfpc  27104  bcmono  27245  gausslemma2dlem1a  27333  gausslemma2dlem2  27335  gausslemma2dlem4  27337  2lgsoddprmlem3  27382  pntrmax  27532  qabvexp  27594  ostth2lem2  27602  nosepon  27634  nolesgn2o  27640  nogesgn1o  27642  nosepnelem  27648  nosepne  27649  nosepdmlem  27652  nosepdm  27653  nodenselem8  27660  noresle  27666  noetasuplem4  27705  noetainflem4  27709  scutbdaylt  27787  addsuniflem  27965  ssltmul1  28107  precsexlem6  28171  precsexlem7  28172  precsexlem11  28176  sltonold  28219  onnolt  28224  n0sfincut  28303  expadds  28377  ax5seglem4  28916  axeuclidlem  28946  uhgredgrnv  29114  usgredg4  29201  nbuhgr2vtx1edgblem  29335  vtxduhgr0e  29463  vtxduhgr0nedg  29477  rusgrpropnb  29568  uspgr2wlkeqi  29633  redwlklem  29656  lfgrwlkprop  29672  2pthnloop  29718  spthonepeq  29739  pthdlem2lem  29754  crctcshwlkn0lem3  29799  crctcshwlkn0lem5  29801  crctcshwlkn0lem7  29803  crctcshwlkn0  29808  wlkiswwlks1  29854  wlkiswwlks2  29862  wlkiswwlksupgr2  29864  wwlksnext  29880  wwlksnextproplem2  29897  wspthsnonn0vne  29904  2pthon3v  29930  rusgrnumwwlk  29962  erclwwlkeqlen  30005  erclwwlksym  30007  erclwwlktr  30008  erclwwlkneqlen  30054  erclwwlknsym  30056  erclwwlkntr  30057  uhgr3cyclex  30168  upgreupthseg  30195  eupth2lem3lem4  30217  eucrctshift  30229  4cycl2vnunb  30276  nvs  30649  nvtri  30656  nmlno0  30781  nmlnoubi  30782  ubth  30859  hlipgt0  30900  ocnel  31284  elspansn2  31553  elspansn3  31558  normcan  31562  pjoml2  31597  lecm  31603  osum  31631  nmbdfnlb  32036  leopmul  32120  hstpyth  32215  cvnbtwn  32272  ssmd1  32297  ssmd2  32298  ssdmd1  32299  ssdmd2  32300  cvmd  32322  cvdmd  32323  superpos  32340  disji2f  32563  disjif  32564  disjif2  32567  preiman0  32692  padct  32702  ffs2  32710  bcm1n  32777  sgn3da  32818  s2f1  32925  omndadd  33079  ogrpaddlt  33090  archiabl  33201  slmdlema  33205  lbslsat  33661  eulerpartlemb  34405  fisshasheq  35142  cvmsdisj  35297  cvmlift2lem12  35341  satfrel  35394  satfrnmapom  35397  fmlasuc  35413  satffun  35436  satef  35443  sategoelfv  35447  lineintmo  36180  nn0prpwlem  36345  nn0prpw  36346  neibastop2lem  36383  lindsadd  37642  areacirc  37742  incsequz  37777  mettrifi  37786  ismtybnd  37836  heiborlem1  37840  rngoisocnv  38010  risci  38016  eqvrelqsel  38639  lfl1  39093  lkrlsp2  39126  omlfh3N  39282  cvrnbtwn  39294  cvrnbtwn2  39298  cvrnbtwn4  39302  cvlexch3  39355  cvlexch4N  39356  cvlatexchb1  39357  2llnne2N  39432  atcvrj0  39452  cvrat2  39453  ps-1  39501  3atlem5  39511  islln2a  39541  lplnriaN  39574  lplnribN  39575  llncvrlpln2  39581  lplncvrlvol2  39639  psubatN  39779  pmapglb2N  39795  pmapglb2xN  39796  2llnma1b  39810  paddasslem17  39860  pmod2iN  39873  pmodl42N  39875  hlmod1i  39880  atmod1i1  39881  atmod1i2  39883  llnmod1i2  39884  pclcmpatN  39925  osumcllem8N  39987  pexmidlem3N  39996  pl42lem4N  40006  4atexlem7  40099  ltrnnid  40160  cdlemc4  40218  cdleme32a  40465  cdlemeg46gfre  40556  cdlemf2  40586  cdlemg4c  40636  trlcoat  40747  tendovalco  40789  tendoeq2  40798  cdlemk36  40937  diael  41067  diatrl  41068  dicelval1stN  41212  dicelval2nd  41213  dihlspsnat  41357  dochkr1  41502  lcfrlem9  41574  mapdh8e  41808  hdmapval0  41857  hgmapval0  41916  nnadddir  42288  dvdsexpnn0  42352  incssnn0  42709  pell14qrexpcl  42865  pell14qrgap  42873  congadd  42965  acongsym  42975  acongtr  42977  dvdsacongtr  42983  jm2.19lem3  42990  jm2.19lem4  42991  jm2.26lem3  43000  onexlimgt  43242  nadd2rabex  43385  ismnushort  44300  bi13impia  44489  3impcombi  44816  ioogtlb  45504  iocgtlb  45511  iocleub  45512  icoltub  45517  iooltub  45519  limclner  45660  limsupre3lem  45741  climuzlem  45752  fsupdm  46851  finfdm  46855  elfzelfzlble  47330  subsubelfzo0  47335  m1modnep2mod  47361  iccpartigtl  47417  sqrtpwpw2p  47532  fmtnoprmfac1lem  47558  fmtno4prmfac  47566  evenltle  47711  even3prm2  47713  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  bgoldbtbndlem1  47799  bgoldbtbndlem3  47801  bgoldbtbndlem4  47802  bgoldbtbnd  47803  uhgrimisgrgriclem  47923  isubgr3stgrlem7  47964  clnbgr3stgrgrlic  48004  upgrwlkupwlk  48095  funcringcsetcALTV2lem9  48253  funcringcsetclem9ALTV  48276  lincscmcl  48388  lindslinindimp2lem4  48417  lincresunit2  48434  lincresunit3  48437  elfzolborelfzop1  48475  m1modmmod  48481  rege1logbzge0  48519  fllog2  48528  dignn0ldlem  48562  rrx2pnecoorneor  48675  rrx2plord2  48682  rrx2linest  48702  ipolub  48942  ipoglb  48945